--- a/src/Pure/Tools/build.ML Sat Nov 14 17:29:37 2020 +0100
+++ b/src/Pure/Tools/build.ML Sun Nov 15 17:34:19 2020 +0100
@@ -55,11 +55,10 @@
(* build theories *)
-fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) =
+fun build_theories symbols last_timing qualifier master_dir (options, thys) =
let
val context =
- {options = options, symbols = symbols, bibtex_entries = bibtex_entries,
- last_timing = last_timing};
+ {options = options, symbols = symbols, last_timing = last_timing};
val condition = space_explode "," (Options.string options "condition");
val conds = filter_out (can getenv_strict) condition;
in
@@ -104,7 +103,8 @@
(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 (pair string (list string)))))))))))))))))
end;
val symbols = HTML.make_symbols symbol_codes;
@@ -115,6 +115,7 @@
Resources.init_session
{session_positions = session_positions,
session_directories = session_directories,
+ bibtex_entries = bibtex_entries,
docs = doc_names,
global_theories = global_theories,
loaded_theories = loaded_theories};
@@ -133,8 +134,7 @@
val res1 =
theories |>
- (List.app
- (build_theories symbols bibtex_entries last_timing session_name master_dir)
+ (List.app (build_theories symbols last_timing session_name master_dir)
|> session_timing
|> Exn.capture);
val res2 = Exn.capture Session.finish ();