--- a/src/Pure/Tools/build.ML Sat Apr 08 12:47:34 2017 +0200
+++ b/src/Pure/Tools/build.ML Sat Apr 08 20:56:41 2017 +0200
@@ -145,6 +145,8 @@
name: string,
master_dir: Path.T,
theories: (Options.T * (string * Position.T) list) list,
+ global_theories: string list,
+ loaded_theories: (string * string) list,
known_theories: (string * string) list};
fun decode_args yxml =
@@ -152,12 +154,13 @@
open XML.Decode;
val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
(document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
- (theories, known_theories)))))))))))) =
+ (theories, (global_theories, (loaded_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
(pair (((list (pair Options.decode (list (string #> rpair Position.none))))))
- (list (pair string string)))))))))))))
+ (pair (list string)
+ (pair (list (pair string string)) (list (pair string string)))))))))))))))
(YXML.parse_body yxml);
in
Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
@@ -165,15 +168,22 @@
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,
+ global_theories = global_theories, loaded_theories = loaded_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, known_theories}) =
+ document_files, graph_file, parent_name, chapter, name, master_dir, theories,
+ global_theories, loaded_theories, known_theories}) =
let
val symbols = HTML.make_symbols symbol_codes;
- val _ = Resources.set_session_base {known_theories = known_theories};
+ val _ =
+ Resources.set_session_base
+ {default_qualifier = name,
+ global_theories = global_theories,
+ loaded_theories = loaded_theories,
+ known_theories = known_theories};
val _ =
Session.init