--- a/src/Pure/Tools/build.ML Mon Feb 29 15:39:17 2016 +0100
+++ b/src/Pure/Tools/build.ML Mon Feb 29 16:12:47 2016 +0100
@@ -124,15 +124,16 @@
let
val _ = SHA1_Samples.test ();
- val (symbol_codes, (command_timings, (do_output, (options, (verbose, (browser_info,
+ val (symbol_codes, (command_timings, (output, (options, (verbose, (browser_info,
(document_files, (graph_file, (parent_name, (chapter, (name, theories))))))))))) =
File.read (Path.explode args_file) |> YXML.parse_body |>
let open XML.Decode in
- pair (list (pair string int)) (pair (list properties) (pair bool (pair Options.decode
+ pair (list (pair string int)) (pair (list properties) (pair string (pair Options.decode
(pair bool (pair string (pair (list (pair string string)) (pair string
(pair string (pair string (pair string
((list (pair Options.decode (list (string #> rpair Position.none)))))))))))))))
end;
+ val do_output = output <> "";
val symbols = HTML.make_symbols symbol_codes;
val _ = Options.set_default options;
@@ -165,7 +166,8 @@
val _ = Par_Exn.release_all [res1, res2];
val _ = Options.reset_default ();
- val _ = if do_output then () else exit 0;
+ val _ = Session.shutdown ();
+ val _ = if do_output then (ML_Heap.share_common_data (); ML_Heap.save_state output) else ();
in () end);