refer to HTML symbols via resources;
authorwenzelm
Mon, 16 Nov 2020 13:11:15 +0100
changeset 72859 429afd0d1a79
parent 72856 4b2691211719
child 72860 65554bac121b
refer to HTML symbols via resources;
src/Pure/ML/ml_process.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/resources.ML
src/Pure/PIDE/session.ML
src/Pure/Thy/present.ML
src/Pure/Thy/thy_info.ML
src/Pure/Tools/build.ML
--- a/src/Pure/ML/ml_process.scala	Sun Nov 15 16:51:58 2020 +0000
+++ b/src/Pure/ML/ml_process.scala	Mon Nov 16 13:11:15 2020 +0100
@@ -85,6 +85,9 @@
       session_base match {
         case None => ""
         case Some(base) =>
+          def print_symbols: List[(String, Int)] => String =
+            ML_Syntax.print_list(
+              ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_int))
           def print_table: List[(String, String)] => String =
             ML_Syntax.print_list(
               ML_Syntax.print_pair(
@@ -100,7 +103,8 @@
                 ML_Syntax.print_list(ML_Syntax.print_string_bytes)))
 
           "Resources.init_session" +
-            "{session_positions = " + print_sessions(sessions_structure.session_positions) +
+            "{html_symbols = " + print_symbols(Symbol.codes) +
+            ", session_positions = " + print_sessions(sessions_structure.session_positions) +
             ", session_directories = " + print_table(sessions_structure.dest_session_directories) +
             ", session_chapters = " + print_table(sessions_structure.session_chapters) +
             ", bibtex_entries = " + print_bibtex_entries(sessions_structure.bibtex_entries) +
--- a/src/Pure/PIDE/protocol.ML	Sun Nov 15 16:51:58 2020 +0000
+++ b/src/Pure/PIDE/protocol.ML	Mon Nov 16 13:11:15 2020 +0100
@@ -25,9 +25,10 @@
 
 val _ =
   Isabelle_Process.protocol_command "Prover.init_session"
-    (fn [session_positions_yxml, session_directories_yxml, session_chapters_yxml,
+    (fn [html_symbols_yxml, session_positions_yxml, session_directories_yxml, session_chapters_yxml,
           bibtex_entries_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml] =>
       let
+        val decode_symbols = YXML.parse_body #> let open XML.Decode in list (pair string int) end;
         val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
         val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
         val decode_sessions =
@@ -36,7 +37,8 @@
           YXML.parse_body #> let open XML.Decode in list (pair string (list string)) end;
       in
         Resources.init_session
-          {session_positions = decode_sessions session_positions_yxml,
+          {html_symbols = decode_symbols html_symbols_yxml,
+           session_positions = decode_sessions session_positions_yxml,
            session_directories = decode_table session_directories_yxml,
            session_chapters = decode_table session_chapters_yxml,
            bibtex_entries = decode_bibtex_entries bibtex_entries_yxml,
--- 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;
--- a/src/Pure/PIDE/session.ML	Sun Nov 15 16:51:58 2020 +0000
+++ b/src/Pure/PIDE/session.ML	Mon Nov 16 13:11:15 2020 +0100
@@ -9,7 +9,7 @@
   val get_name: unit -> string
   val welcome: unit -> string
   val get_keywords: unit -> Keyword.keywords
-  val init: HTML.symbols -> bool -> Path.T -> string list -> string -> string * string -> bool -> unit
+  val init: bool -> Path.T -> string list -> string -> string * string -> bool -> unit
   val shutdown: unit -> unit
   val finish: unit -> unit
 end;
@@ -45,12 +45,12 @@
 
 (* init *)
 
-fun init symbols info info_path documents parent (chapter, name) verbose =
+fun init info info_path documents parent (chapter, name) verbose =
   (Synchronized.change session (fn ({name = parent_name, ...}, parent_finished) =>
     if parent_name <> parent orelse not parent_finished then
       error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
     else ({chapter = chapter, name = name}, false));
-    Present.init symbols info info_path documents (chapter, name) verbose);
+    Present.init info info_path documents (chapter, name) verbose);
 
 
 (* finish *)
--- a/src/Pure/Thy/present.ML	Sun Nov 15 16:51:58 2020 +0000
+++ b/src/Pure/Thy/present.ML	Mon Nov 16 13:11:15 2020 +0100
@@ -6,9 +6,9 @@
 
 signature PRESENT =
 sig
-  val init: HTML.symbols -> bool -> Path.T -> string list -> string * string -> bool -> unit
+  val init: bool -> Path.T -> string list -> string * string -> bool -> unit
   val finish: unit -> unit
-  val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
+  val begin_theory: int -> HTML.text -> theory -> theory
 end;
 
 structure Present: PRESENT =
@@ -61,12 +61,11 @@
 (* session_info *)
 
 type session_info =
-  {symbols: HTML.symbols, name: string, chapter: string, info_path: Path.T, info: bool,
+  {name: string, chapter: string, info_path: Path.T, info: bool,
     verbose: bool, readme: Path.T option};
 
-fun make_session_info
-  (symbols, name, chapter, info_path, info, verbose, readme) =
-  {symbols = symbols, name = name, chapter = chapter, info_path = info_path, info = info,
+fun make_session_info (name, chapter, info_path, info, verbose, readme) =
+  {name = name, chapter = chapter, info_path = info_path, info = info,
     verbose = verbose, readme = readme}: session_info;
 
 
@@ -88,16 +87,15 @@
 
 (* init session *)
 
-fun init symbols info info_path documents (chapter, name) verbose =
+fun init info info_path documents (chapter, name) verbose =
   let
     val readme = if File.exists readme_html_path then SOME readme_html_path else NONE;
-
+    val symbols = Resources.html_symbols ();
     val docs =
       (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
         map (fn name => (Url.File (document_path name), name)) documents;
   in
-    session_info :=
-      SOME (make_session_info (symbols, name, chapter, info_path, info, verbose, readme));
+    session_info := SOME (make_session_info (name, chapter, info_path, info, verbose, readme));
     Synchronized.change browser_info (K empty_browser_info);
     add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs)
   end;
@@ -148,8 +146,8 @@
     else SOME (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 {symbols, name = session_name, chapter, ...} =>
+fun begin_theory update_time html thy =
+  with_session_info thy (fn {name = session_name, chapter, ...} =>
     let
       val name = Context.theory_name thy;
 
@@ -158,7 +156,8 @@
           (Option.map Url.File (theory_link (chapter, session_name) parent),
             (Context.theory_name parent)));
 
-      val _ = update_html name (HTML.theory symbols name parent_specs (mk_text ()));
+      val symbols = Resources.html_symbols ();
+      val _ = update_html name (HTML.theory symbols name parent_specs html);
 
       val _ =
         if is_session_theory thy then
--- 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)
--- a/src/Pure/Tools/build.ML	Sun Nov 15 16:51:58 2020 +0000
+++ b/src/Pure/Tools/build.ML	Mon Nov 16 13:11:15 2020 +0100
@@ -55,10 +55,9 @@
 
 (* build theories *)
 
-fun build_theories symbols last_timing qualifier master_dir (options, thys) =
+fun build_theories last_timing qualifier master_dir (options, thys) =
   let
-    val context =
-      {options = options, symbols = symbols, last_timing = last_timing};
+    val context = {options = options, last_timing = last_timing};
     val condition = space_explode "," (Options.string options "condition");
     val conds = filter_out (can getenv_strict) condition;
   in
@@ -87,7 +86,7 @@
   Isabelle_Process.protocol_command "build_session"
     (fn [args_yxml] =>
         let
-          val (symbol_codes, (command_timings, (verbose, (browser_info,
+          val (html_symbols, (command_timings, (verbose, (browser_info,
             (documents, (parent_name, (chapter, (session_name, (master_dir,
             (theories, (session_positions, (session_directories, (session_chapters,
             (doc_names, (global_theories, (loaded_theories, bibtex_entries)))))))))))))))) =
@@ -108,13 +107,12 @@
                                 (list (pair string (list string))))))))))))))))))
               end;
 
-          val symbols = HTML.make_symbols symbol_codes;
-
           fun build () =
             let
               val _ =
                 Resources.init_session
-                  {session_positions = session_positions,
+                  {html_symbols = html_symbols,
+                   session_positions = session_positions,
                    session_directories = session_directories,
                    session_chapters = session_chapters,
                    bibtex_entries = bibtex_entries,
@@ -124,7 +122,6 @@
 
               val _ =
                 Session.init
-                  symbols
                   (Options.default_bool "browser_info")
                   browser_info
                   documents
@@ -136,7 +133,7 @@
 
               val res1 =
                 theories |>
-                  (List.app (build_theories symbols last_timing session_name master_dir)
+                  (List.app (build_theories last_timing session_name master_dir)
                     |> session_timing
                     |> Exn.capture);
               val res2 = Exn.capture Session.finish ();