1 (* Title: Pure/System/build.ML
4 Build Isabelle sessions.
9 val build: string -> unit
12 structure Build: BUILD =
17 fun use_thys options =
19 |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
20 |> Unsynchronized.setmp print_mode
21 (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
22 |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
23 |> Unsynchronized.setmp Goal.parallel_proofs_threshold
24 (Options.int options "parallel_proofs_threshold")
25 |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
26 |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
27 |> Options.bool options "no_document" ? Present.no_document
28 |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty");
30 fun use_theories (options, thys) =
31 let val condition = space_explode "," (Options.string options "condition") in
32 (case filter_out (can getenv_strict) condition of
33 [] => use_thys options thys
35 Output.physical_stderr ("Ignoring theories " ^ commas_quote thys ^
36 " (missing " ^ commas conds ^ ")\n"))
43 val (save, (options, (timing, (verbose, (browser_info, (parent,
44 (name, (base_name, theories)))))))) =
45 File.read (Path.explode args_file) |> YXML.parse_body |>
46 let open XML.Decode in
47 pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string
48 (pair string (pair string ((list (pair Options.decode (list string)))))))))))
52 Session.init save false
53 (Options.bool options "browser_info") browser_info
54 (Options.string options "document")
55 (Options.bool options "document_graph")
56 (space_explode ":" (Options.string options "document_variants"))
58 (true (* FIXME copy document/ files on Scala side!? *),
59 Options.string options "document_dump")
60 (Options.string options "browser_info_remote")
63 val _ = Session.with_timing name timing (List.app use_theories) theories;
64 val _ = Session.finish ();
66 val _ = if save then () else quit ();
68 handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);