1 (* Title: Pure/System/build.ML
4 Build Isabelle sessions.
9 val build: string -> unit
12 structure Build: BUILD =
15 fun use_theories options =
17 |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
18 |> Unsynchronized.setmp print_mode
19 (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
20 |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
21 |> Unsynchronized.setmp Goal.parallel_proofs_threshold
22 (Options.int options "parallel_proofs_threshold")
23 |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
24 |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
25 |> Options.bool options "no_document" ? Present.no_document
26 |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty");
30 val (save, (options, (timing, (verbose, (browser_info, (parent,
31 (name, (base_name, theories)))))))) =
32 File.read (Path.explode args_file) |> YXML.parse_body |>
33 let open XML.Decode in
34 pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string
35 (pair string (pair string ((list (pair Options.decode (list string)))))))))))
39 Session.init save false
40 (Options.bool options "browser_info") browser_info
41 (Options.string options "document")
42 (Options.bool options "document_graph")
43 (space_explode "," (Options.string options "document_variants"))
45 (true (* FIXME copy document/ files on Scala side!? *),
46 Options.string options "document_dump")
47 (Options.string options "browser_info_remote")
50 val _ = Session.with_timing name timing (List.app (uncurry use_theories)) theories;
51 val _ = Session.finish ();
53 val _ = if save then () else quit ();
55 handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);