--- a/src/Pure/Tools/build.ML Sun Nov 15 16:51:58 2020 +0000
+++ b/src/Pure/Tools/build.ML Mon Nov 16 13:11:15 2020 +0100
@@ -55,10 +55,9 @@
(* build theories *)
-fun build_theories symbols last_timing qualifier master_dir (options, thys) =
+fun build_theories last_timing qualifier master_dir (options, thys) =
let
- val context =
- {options = options, symbols = symbols, last_timing = last_timing};
+ val context = {options = options, last_timing = last_timing};
val condition = space_explode "," (Options.string options "condition");
val conds = filter_out (can getenv_strict) condition;
in
@@ -87,7 +86,7 @@
Isabelle_Process.protocol_command "build_session"
(fn [args_yxml] =>
let
- val (symbol_codes, (command_timings, (verbose, (browser_info,
+ val (html_symbols, (command_timings, (verbose, (browser_info,
(documents, (parent_name, (chapter, (session_name, (master_dir,
(theories, (session_positions, (session_directories, (session_chapters,
(doc_names, (global_theories, (loaded_theories, bibtex_entries)))))))))))))))) =
@@ -108,13 +107,12 @@
(list (pair string (list string))))))))))))))))))
end;
- val symbols = HTML.make_symbols symbol_codes;
-
fun build () =
let
val _ =
Resources.init_session
- {session_positions = session_positions,
+ {html_symbols = html_symbols,
+ session_positions = session_positions,
session_directories = session_directories,
session_chapters = session_chapters,
bibtex_entries = bibtex_entries,
@@ -124,7 +122,6 @@
val _ =
Session.init
- symbols
(Options.default_bool "browser_info")
browser_info
documents
@@ -136,7 +133,7 @@
val res1 =
theories |>
- (List.app (build_theories symbols last_timing session_name master_dir)
+ (List.app (build_theories last_timing session_name master_dir)
|> session_timing
|> Exn.capture);
val res2 = Exn.capture Session.finish ();