src/Pure/PIDE/resources.ML

--- a/src/Pure/PIDE/resources.ML	Sun Nov 15 16:51:58 2020 +0000
+++ b/src/Pure/PIDE/resources.ML	Mon Nov 16 13:11:15 2020 +0100
@@ -8,7 +8,8 @@
 sig
   val default_qualifier: string
   val init_session:
-    {session_positions: (string * Properties.T) list,
+    {html_symbols: (string * int) list,
+     session_positions: (string * Properties.T) list,
      session_directories: (string * string) list,
      session_chapters: (string * string) list,
      bibtex_entries: (string * string list) list,
@@ -18,6 +19,7 @@
   val finish_session_base: unit -> unit
   val global_theory: string -> string option
   val loaded_theory: string -> bool
+  val html_symbols: unit -> HTML.symbols
   val check_session: Proof.context -> string * Position.T -> string
   val session_chapter: string -> string
   val check_doc: Proof.context -> string * Position.T -> string
@@ -56,7 +58,8 @@
   {pos = Position.of_properties props, serial = serial ()};
 
 val empty_session_base =
-  {session_positions = []: (string * entry) list,
+  {html_symbols = HTML.no_symbols,
+   session_positions = []: (string * entry) list,
    session_directories = Symtab.empty: Path.T list Symtab.table,
    session_chapters = Symtab.empty: string Symtab.table,
    bibtex_entries = Symtab.empty: string list Symtab.table,
@@ -68,11 +71,12 @@
   Synchronized.var "Sessions.base" empty_session_base;
 
 fun init_session
-    {session_positions, session_directories, session_chapters,
+    {html_symbols, session_positions, session_directories, session_chapters,
       bibtex_entries, docs, global_theories, loaded_theories} =
   Synchronized.change global_session_base
     (fn _ =>
-      {session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
+      {html_symbols = HTML.make_symbols html_symbols,
+       session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
        session_directories =
          fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))
            session_directories Symtab.empty,
@@ -85,7 +89,8 @@
 fun finish_session_base () =
   Synchronized.change global_session_base
     (fn {global_theories, loaded_theories, ...} =>
-      {session_positions = [],
+      {html_symbols = HTML.no_symbols,
+       session_positions = [],
        session_directories = Symtab.empty,
        session_chapters = Symtab.empty,
        bibtex_entries = Symtab.empty,
@@ -98,6 +103,7 @@
 fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
 fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
 
+fun html_symbols () = get_session_base #html_symbols;
 
 fun check_name which kind markup ctxt arg =
   Completion.check_item kind markup (get_session_base which |> sort_by #1) ctxt arg;