1 (* Title: Pure/System/build.ML
4 Build Isabelle sessions.
9 val build: string -> unit
12 structure Build: BUILD =
17 fun no_document options =
18 (case Options.string options "document" of "" => true | "false" => true | _ => false) andalso
19 (Options.string options "document_dump" = "");
21 fun use_thys options =
23 |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
24 |> Unsynchronized.setmp print_mode
25 (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
26 |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
27 |> Unsynchronized.setmp Goal.parallel_proofs_threshold
28 (Options.int options "parallel_proofs_threshold")
29 |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
30 |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
31 |> no_document options ? Present.no_document
32 |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
33 |> Unsynchronized.setmp Printer.show_question_marks_default
34 (Options.bool options "show_question_marks")
35 |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
36 |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
37 |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
38 |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
40 fun use_theories (options, thys) =
41 let val condition = space_explode "," (Options.string options "condition") in
42 (case filter_out (can getenv_strict) condition of
43 [] => use_thys options thys
45 Output.physical_stderr ("Ignoring theories " ^ commas_quote thys ^
46 " (undefined " ^ commas conds ^ ")\n"))
53 val (save, (options, (timing, (verbose, (browser_info, (parent_base_name,
54 (name, (base_name, theories)))))))) =
55 File.read (Path.explode args_file) |> YXML.parse_body |>
56 let open XML.Decode in
57 pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string
58 (pair string (pair string ((list (pair Options.decode (list string)))))))))))
62 Session.init save false
63 (Options.bool options "browser_info") browser_info
64 (Options.string options "document")
65 (Options.bool options "document_graph")
66 (space_explode ":" (Options.string options "document_variants"))
67 parent_base_name base_name
68 (not (Options.bool options "document_dump_only"), Options.string options "document_dump")
69 (Options.string options "browser_info_remote")
71 val _ = Session.with_timing name timing (List.app use_theories) theories;
72 val _ = Session.finish ();
73 val _ = if save then () else quit ();
75 handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);