src/Pure/Thy/thy_info.ML

--- a/src/Pure/Thy/thy_info.ML	Fri Oct 09 21:20:43 2015 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sat Oct 10 16:21:34 2015 +0200
@@ -14,8 +14,10 @@
   val master_directory: string -> Path.T
   val remove_thy: string -> unit
   val use_theories:
-    {document: bool, last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} ->
-    (string * Position.T) list -> unit
+    {document: bool,
+     symbols: HTML.symbols,
+     last_timing: Toplevel.transition -> Time.time option,
+     master_dir: Path.T} -> (string * Position.T) list -> unit
   val use_thys: (string * Position.T) list -> unit
   val use_thy: string * Position.T -> unit
   val script_thy: Position.T -> string -> theory -> theory
@@ -237,7 +239,8 @@
 fun required_by _ [] = ""
   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
-fun load_thy document last_timing initiators update_time deps text (name, pos) keywords parents =
+fun load_thy document symbols last_timing
+    initiators update_time deps text (name, pos) keywords parents =
   let
     val _ = remove_thy name;
     val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
@@ -256,7 +259,7 @@
 
     val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
     val (theory, present, weight) =
-      Resources.load_thy document last_timing update_time dir header text_pos text
+      Resources.load_thy document symbols last_timing update_time dir header text_pos text
         (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
     fun commit () = update_thy deps theory;
   in
@@ -283,9 +286,9 @@
 
 in
 
-fun require_thys document last_timing initiators dir strs tasks =
-      fold_map (require_thy document last_timing initiators dir) strs tasks |>> forall I
-and require_thy document last_timing initiators dir (str, require_pos) tasks =
+fun require_thys document symbols last_timing initiators dir strs tasks =
+      fold_map (require_thy document symbols last_timing initiators dir) strs tasks |>> forall I
+and require_thy document symbols last_timing initiators dir (str, require_pos) tasks =
   let
     val path = Path.expand (Path.explode str);
     val name = Path.implode (Path.base path);
@@ -315,7 +318,7 @@
 
           val parents = map (base_name o #1) imports;
           val (parents_current, tasks') =
-            require_thys document last_timing (name :: initiators)
+            require_thys document symbols last_timing (name :: initiators)
               (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
 
           val all_current = current andalso parents_current;
@@ -328,7 +331,7 @@
                   let
                     val update_time = serial ();
                     val load =
-                      load_thy document last_timing initiators update_time dep
+                      load_thy document symbols last_timing initiators update_time dep
                         text (name, theory_pos) keywords;
                   in Task (node_name, parents, load) end);
 
@@ -341,10 +344,14 @@
 
 (* use_thy *)
 
-fun use_theories {document, last_timing, master_dir} imports =
-  schedule_tasks (snd (require_thys document last_timing [] master_dir imports String_Graph.empty));
+fun use_theories {document, symbols, last_timing, master_dir} imports =
+  schedule_tasks
+    (snd (require_thys document symbols last_timing [] master_dir imports String_Graph.empty));
 
-val use_thys = use_theories {document = false, last_timing = K NONE, master_dir = Path.current};
+val use_thys =
+  use_theories
+    {document = false, symbols = HTML.no_symbols, last_timing = K NONE, master_dir = Path.current};
+
 val use_thy = use_thys o single;