--- a/src/Pure/Tools/build.ML Fri Apr 07 18:26:30 2017 +0200
+++ b/src/Pure/Tools/build.ML Fri Apr 07 19:35:39 2017 +0200
@@ -144,30 +144,37 @@
chapter: string,
name: string,
master_dir: Path.T,
- theories: (Options.T * (string * Position.T) list) list};
+ theories: (Options.T * (string * Position.T) list) list,
+ known_theories: (string * string) list};
fun decode_args yxml =
let
open XML.Decode;
val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
- (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir, theories))))))))))) =
+ (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
+ (theories, known_theories)))))))))))) =
pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
(pair (list (pair string string)) (pair string (pair string (pair string (pair string
- (pair string (((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))))
+ (pair string
+ (pair (((list (pair Options.decode (list (string #> rpair Position.none))))))
+ (list (pair string string)))))))))))))
(YXML.parse_body yxml);
in
Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
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,
- name = name, master_dir = Path.explode master_dir, theories = theories}
+ name = name, master_dir = Path.explode master_dir, theories = theories,
+ known_theories = known_theories}
end;
fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
- document_files, graph_file, parent_name, chapter, name, master_dir, theories}) =
+ document_files, graph_file, parent_name, chapter, name, master_dir, theories, known_theories}) =
let
val symbols = HTML.make_symbols symbol_codes;
+ val _ = Resources.set_session_base {known_theories = known_theories};
+
val _ =
Session.init
symbols
@@ -191,6 +198,8 @@
|> session_timing name verbose
|> Exn.capture);
val res2 = Exn.capture Session.finish ();
+
+ val _ = Resources.reset_session_base ();
val _ = Par_Exn.release_all [res1, res2];
in () end;