--- a/src/Pure/Tools/build.ML Sat Mar 28 18:33:25 2020 +0100
+++ b/src/Pure/Tools/build.ML Sat Mar 28 19:11:59 2020 +0100
@@ -133,7 +133,6 @@
datatype args = Args of
{symbol_codes: (string * int) list,
command_timings: Properties.T list,
- do_output: bool,
verbose: bool,
browser_info: Path.T,
document_files: (Path.T * Path.T) list,
@@ -154,20 +153,20 @@
let
open XML.Decode;
val position = Position.of_properties o properties;
- val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
+ val (symbol_codes, (command_timings, (verbose, (browser_info,
(document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
(theories, (session_positions, (session_directories, (doc_names, (global_theories,
- (loaded_theories, bibtex_entries))))))))))))))))) =
- pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
+ (loaded_theories, bibtex_entries)))))))))))))))) =
+ pair (list (pair string int)) (pair (list properties) (pair bool (pair string
(pair (list (pair string string)) (pair string (pair string (pair string (pair string
(pair string
(pair (((list (pair Options.decode (list (pair string position))))))
(pair (list (pair string properties))
(pair (list (pair string string)) (pair (list string)
- (pair (list (pair string string)) (pair (list string) (list string)))))))))))))))))
+ (pair (list (pair string string)) (pair (list string) (list string))))))))))))))))
(YXML.parse_body yxml);
in
- Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
+ Args {symbol_codes = symbol_codes, command_timings = command_timings,
verbose = verbose, browser_info = Path.explode browser_info,
document_files = map (apply2 Path.explode) document_files,
graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
@@ -177,7 +176,7 @@
bibtex_entries = bibtex_entries}
end;
-fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
+fun build_session (Args {symbol_codes, command_timings, verbose, browser_info,
document_files, graph_file, parent_name, chapter, name, master_dir, theories, session_positions,
session_directories, doc_names, global_theories, loaded_theories, bibtex_entries}) =
let
@@ -194,7 +193,6 @@
val _ =
Session.init
symbols
- do_output
(Options.default_bool "browser_info")
browser_info
(Options.default_string "document")