src/Pure/Thy/present.ML

 sig
   val session_name: theory -> string
   val session_graph: string -> (string -> bool) -> theory -> Graph_Display.entry list
   val document_enabled: string -> bool
   val document_variants: string -> (string * string) list
-  val init: bool -> bool -> Path.T -> string -> string -> (string * string) list ->
+  val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
     (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
   val finish: unit -> unit
   val theory_output: string -> string -> unit
   val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
   val display_drafts: Path.T list -> int

 (** global session state **)
 
 (* session_info *)
 
 type session_info =
-  {name: string, chapter: string, info_path: Path.T, info: bool, doc_format: string,
-    doc_output: Path.T option, doc_files: (Path.T * Path.T) list, graph_file: Path.T,
-    documents: (string * string) list, verbose: bool, readme: Path.T option};
+  {symbols: HTML.symbols, name: string, chapter: string, info_path: Path.T, info: bool,
+    doc_format: string, doc_output: Path.T option, doc_files: (Path.T * Path.T) list,
+    graph_file: Path.T, documents: (string * string) list, verbose: bool, readme: Path.T option};
 
 fun make_session_info
-  (name, chapter, info_path, info, doc_format, doc_output, doc_files,
+  (symbols, name, chapter, info_path, info, doc_format, doc_output, doc_files,
     graph_file, documents, verbose, readme) =
-  {name = name, chapter = chapter, info_path = info_path, info = info, doc_format = doc_format,
-    doc_output = doc_output, doc_files = doc_files, graph_file = graph_file,
+  {symbols = symbols, name = name, chapter = chapter, info_path = info_path, info = info,
+    doc_format = doc_format, doc_output = doc_output, doc_files = doc_files, graph_file = graph_file,
     documents = documents, verbose = verbose, readme = readme}: session_info;
 
 
 (* state *)
 

   in variants end;
 
 
 (* init session *)
 
-fun init build info info_path doc document_output doc_variants doc_files graph_file
+fun init symbols build info info_path doc document_output doc_variants doc_files graph_file
     (chapter, name) verbose =
   if not build andalso not info andalso doc = "" then
     (Synchronized.change browser_info (K empty_browser_info); session_info := NONE)
   else
     let

       val docs =
         (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
           map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
     in
       session_info :=
-        SOME (make_session_info (name, chapter, info_path, info, doc,
+        SOME (make_session_info (symbols, name, chapter, info_path, info, doc,
           doc_output, doc_files, graph_file, documents, verbose, readme));
       Synchronized.change browser_info (K empty_browser_info);
-      add_html_index (0, HTML.begin_session_index name (Url.File session_graph_path) docs)
+      add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs)
     end;
 
 
 (* isabelle tool wrappers *)
 

     else if chapter = Context.PureN then NONE
     else SOME (Path.appends [Path.parent, Path.parent, Path.basic chapter, Path.basic session, link])
   end;
 
 fun begin_theory update_time mk_text thy =
-  with_session_info thy (fn {name = session_name, chapter, ...} =>
+  with_session_info thy (fn {symbols, name = session_name, chapter, ...} =>
     let
       val name = Context.theory_name thy;
       val parents = Theory.parents_of thy;
 
       val parent_specs = parents |> map (fn parent =>
         (Option.map Url.File (theory_link (chapter, session_name) parent),
           (Context.theory_name parent)));
-      val html_source = HTML.theory name parent_specs (mk_text ());
+      val html_source = HTML.theory symbols name parent_specs (mk_text ());
     in
       init_theory_info name (make_theory_info ("", html_source));
-      add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
+      add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name));
       add_tex_index (update_time, Latex.theory_entry name);
       Browser_Info.put {chapter = chapter, name = session_name} thy
     end);