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 |> (case Options.string options "document" of "" => true | "false" => true | _ => false) ?
29 |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
30 |> Unsynchronized.setmp Printer.show_question_marks_default
31 (Options.bool options "show_question_marks")
32 |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
33 |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
34 |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
35 |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
37 fun use_theories (options, thys) =
38 let val condition = space_explode "," (Options.string options "condition") in
39 (case filter_out (can getenv_strict) condition of
40 [] => use_thys options thys
42 Output.physical_stderr ("Ignoring theories " ^ commas_quote thys ^
43 " (undefined " ^ commas conds ^ ")\n"))
50 val (save, (options, (timing, (verbose, (browser_info, (parent_base_name,
51 (name, (base_name, theories)))))))) =
52 File.read (Path.explode args_file) |> YXML.parse_body |>
53 let open XML.Decode in
54 pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string
55 (pair string (pair string ((list (pair Options.decode (list string)))))))))))
59 Session.init save false
60 (Options.bool options "browser_info") browser_info
61 (Options.string options "document")
62 (Options.bool options "document_graph")
63 (space_explode ":" (Options.string options "document_variants"))
64 parent_base_name base_name
65 (not (Options.bool options "document_dump_only"), Options.string options "document_dump")
66 (Options.string options "browser_info_remote")
68 val _ = Session.with_timing name timing (List.app use_theories) theories;
69 val _ = Session.finish ();
70 val _ = if save then () else quit ();
72 handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);