src/Pure/Thy/thy_info.ML

--- a/src/Pure/Thy/thy_info.ML	Sun Nov 15 16:51:58 2020 +0000
+++ b/src/Pure/Thy/thy_info.ML	Mon Nov 16 13:11:15 2020 +0100
@@ -18,10 +18,7 @@
   val get_theory: string -> theory
   val master_directory: string -> Path.T
   val remove_thy: string -> unit
-  type context =
-    {options: Options.T,
-     symbols: HTML.symbols,
-     last_timing: Toplevel.transition -> Time.time}
+  type context = {options: Options.T, last_timing: Toplevel.transition -> Time.time}
   val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit
   val use_thy: string -> unit
   val script_thy: Position.T -> string -> theory -> theory
@@ -66,6 +63,7 @@
           let
             val thy_name = Context.theory_name thy;
             val document_tex_name = Path.explode_binding0 ("document/" ^ thy_name ^ ".tex");
+
             val latex = Latex.isabelle_body thy_name body;
             val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
           in Export.export thy document_tex_name (XML.blob output) end
@@ -183,15 +181,10 @@
 
 (* context *)
 
-type context =
-  {options: Options.T,
-   symbols: HTML.symbols,
-   last_timing: Toplevel.transition -> Time.time};
+type context = {options: Options.T, last_timing: Toplevel.transition -> Time.time};
 
 fun default_context (): context =
-  {options = Options.default (),
-   symbols = HTML.no_symbols,
-   last_timing = K Time.zeroTime};
+  {options = Options.default (), last_timing = K Time.zeroTime};
 
 
 (* scheduling loader tasks *)
@@ -300,7 +293,7 @@
 
 fun eval_thy (context: context) update_time master_dir header text_pos text parents =
   let
-    val {options, symbols, last_timing} = context;
+    val {options, last_timing} = context;
     val (name, _) = #name header;
     val keywords =
       fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
@@ -309,10 +302,12 @@
     val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text);
     val elements = Thy_Element.parse_elements keywords spans;
 
+    val symbols = Resources.html_symbols ();
+    val html = implode (map (HTML.present_span symbols keywords) spans);
+
     fun init () =
       Resources.begin_theory master_dir header parents
-      |> Present.begin_theory update_time
-        (fn () => implode (map (HTML.present_span symbols keywords) spans));
+      |> Present.begin_theory update_time html;
 
     val (results, thy) =
       cond_timeit true ("theory " ^ quote name)