clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;
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;
29 val (save, (options, (timing, (verbose, (browser_info, (parent,
30 (name, (base_name, theories)))))))) =
31 File.read (Path.explode args_file) |> YXML.parse_body |>
32 let open XML.Decode in
33 pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string
34 (pair string (pair string ((list (pair Options.decode (list string)))))))))))
38 Session.init save false
39 (Options.bool options "browser_info") browser_info
40 (Options.string options "document")
41 (Options.bool options "document_graph")
42 (space_explode "," (Options.string options "document_variants"))
44 (true (* FIXME copy document/ files on Scala side!? *),
45 Options.string options "document_dump")
49 val _ = Session.with_timing name timing (List.app (uncurry use_theories)) theories;
50 val _ = Session.finish ();
52 val _ = if save then () else quit ();
54 handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);