src/Pure/Thy/thy_info.ML

   val get_theory: string -> theory
   val pure_theory: unit -> theory
   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
   val register_thy: theory -> unit
   val finish: unit -> unit

 local
 
 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);
     val _ = Output.try_protocol_message (Markup.loading_theory name) [];
 

       Execution.running Document_ID.none exec_id [] orelse
         raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id);
 
     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
     Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
   end;

             | SOME theory => Resources.loaded_files_current theory);
       in (current, deps', theory_pos', imports', keywords') end);
 
 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);
     val node_name = File.full_path dir (Resources.thy_path path);
     fun check_entry (Task (node_name', _, _)) =

                 ("The error(s) above occurred for theory " ^ quote name ^
                   Position.here require_pos ^ required_by "\n" initiators);
 
           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;
           val task =
             if all_current then Finished (get_theory name)

                 NONE => raise Fail "Malformed deps"
               | SOME (dep, text) =>
                   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);
 
           val tasks'' = new_entry name parents task tasks';
         in (all_current, tasks'') end)

 end;
 
 
 (* 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));
-
-val use_thys = use_theories {document = false, last_timing = K NONE, master_dir = Path.current};
+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, symbols = HTML.no_symbols, last_timing = K NONE, master_dir = Path.current};
+
 val use_thy = use_thys o single;
 
 
 (* toplevel scripting -- without maintaining database *)