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");
36 fun use_theories (options, thys) =
37 let val condition = space_explode "," (Options.string options "condition") in
38 (case filter_out (can getenv_strict) condition of
39 [] => use_thys options thys
41 Output.physical_stderr ("Ignoring theories " ^ commas_quote thys ^
42 " (undefined " ^ commas conds ^ ")\n"))
49 val (save, (options, (timing, (verbose, (browser_info, (parent_base_name,
50 (name, (base_name, theories)))))))) =
51 File.read (Path.explode args_file) |> YXML.parse_body |>
52 let open XML.Decode in
53 pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string
54 (pair string (pair string ((list (pair Options.decode (list string)))))))))))
58 Session.init save false
59 (Options.bool options "browser_info") browser_info
60 (Options.string options "document")
61 (Options.bool options "document_graph")
62 (space_explode ":" (Options.string options "document_variants"))
63 parent_base_name base_name
64 (not (Options.bool options "document_dump_only"), Options.string options "document_dump")
65 (Options.string options "browser_info_remote")
67 val _ = Session.with_timing name timing (List.app use_theories) theories;
68 val _ = Session.finish ();
69 val _ = if save then () else quit ();
71 handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);