refer to session structure from resources;
authorwenzelm
Sun, 15 Nov 2020 22:00:45 +0100
changeset 72853 217e6cf61453
parent 72852 f827c3bb6b7f
child 72854 5fc193537b7c
refer to session structure from resources;
src/Pure/ML/ml_process.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/resources.ML
src/Pure/Thy/present.ML
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
--- a/src/Pure/ML/ml_process.scala	Sun Nov 15 18:16:20 2020 +0100
+++ b/src/Pure/ML/ml_process.scala	Sun Nov 15 22:00:45 2020 +0100
@@ -102,6 +102,7 @@
           "Resources.init_session" +
             "{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) +
             ", docs = " + print_list(base.doc_names) +
             ", global_theories = " + print_table(base.global_theories.toList) +
--- a/src/Pure/PIDE/protocol.ML	Sun Nov 15 18:16:20 2020 +0100
+++ b/src/Pure/PIDE/protocol.ML	Sun Nov 15 22:00:45 2020 +0100
@@ -25,8 +25,8 @@
 
 val _ =
   Isabelle_Process.protocol_command "Prover.init_session"
-    (fn [session_positions_yxml, session_directories_yxml, bibtex_entries_yxml, doc_names_yxml,
-          global_theories_yxml, loaded_theories_yxml] =>
+    (fn [session_positions_yxml, session_directories_yxml, session_chapters_yxml,
+          bibtex_entries_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml] =>
       let
         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;
@@ -38,6 +38,7 @@
         Resources.init_session
           {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,
            docs = decode_list doc_names_yxml,
            global_theories = decode_table global_theories_yxml,
--- a/src/Pure/PIDE/protocol.scala	Sun Nov 15 18:16:20 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala	Sun Nov 15 22:00:45 2020 +0100
@@ -301,6 +301,7 @@
     protocol_command("Prover.init_session",
       encode_sessions(resources.sessions_structure.session_positions),
       encode_table(resources.sessions_structure.dest_session_directories),
+      encode_table(resources.sessions_structure.session_chapters),
       encode_bibtex_entries(resources.sessions_structure.bibtex_entries),
       encode_list(resources.session_base.doc_names),
       encode_table(resources.session_base.global_theories.toList),
--- a/src/Pure/PIDE/resources.ML	Sun Nov 15 18:16:20 2020 +0100
+++ b/src/Pure/PIDE/resources.ML	Sun Nov 15 22:00:45 2020 +0100
@@ -10,6 +10,7 @@
   val init_session:
     {session_positions: (string * Properties.T) list,
      session_directories: (string * string) list,
+     session_chapters: (string * string) list,
      bibtex_entries: (string * string list) list,
      docs: string list,
      global_theories: (string * string) list,
@@ -18,6 +19,7 @@
   val global_theory: string -> string option
   val loaded_theory: string -> bool
   val check_session: Proof.context -> string * Position.T -> string
+  val session_chapter: string -> string
   val check_doc: Proof.context -> string * Position.T -> string
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
@@ -56,6 +58,7 @@
 val empty_session_base =
   {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,
    docs = []: (string * entry) list,
    global_theories = Symtab.empty: string Symtab.table,
@@ -65,14 +68,15 @@
   Synchronized.var "Sessions.base" empty_session_base;
 
 fun init_session
-    {session_positions, session_directories, bibtex_entries, docs,
-      global_theories, loaded_theories} =
+    {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),
        session_directories =
          fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))
            session_directories Symtab.empty,
+       session_chapters = Symtab.make session_chapters,
        bibtex_entries = Symtab.make bibtex_entries,
        docs = sort_by #1 (map (apsnd make_entry o rpair []) docs),
        global_theories = Symtab.make global_theories,
@@ -83,6 +87,7 @@
     (fn {global_theories, loaded_theories, ...} =>
       {session_positions = [],
        session_directories = Symtab.empty,
+       session_chapters = Symtab.empty,
        bibtex_entries = Symtab.empty,
        docs = [],
        global_theories = global_theories,
@@ -103,6 +108,9 @@
       Markup.entity Markup.sessionN name
       |> Markup.properties (Position.entity_properties_of false serial pos));
 
+fun session_chapter name =
+  the_default "Unsorted" (Symtab.lookup (get_session_base #session_chapters) name);
+
 val check_doc = check_name #docs "documentation" (Markup.doc o #1);
 
 
--- a/src/Pure/Thy/present.ML	Sun Nov 15 18:16:20 2020 +0100
+++ b/src/Pure/Thy/present.ML	Sun Nov 15 22:00:45 2020 +0100
@@ -6,7 +6,6 @@
 
 signature PRESENT =
 sig
-  val theory_qualifier: theory -> string
   val init: HTML.symbols -> bool -> Path.T -> string list -> string * string -> bool -> unit
   val finish: unit -> unit
   val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
@@ -29,30 +28,6 @@
 
 
 
-(** theory data **)
-
-type browser_info = {chapter: string, name: string};
-val empty_browser_info: browser_info = {chapter = "Unsorted", name = "Unknown"};
-
-structure Browser_Info = Theory_Data
-(
-  type T = browser_info
-  val empty = empty_browser_info;
-  val extend = I;
-  val merge = #1;
-);
-
-fun reset_browser_info thy =
-  if Browser_Info.get thy = empty_browser_info then NONE
-  else SOME (Browser_Info.put empty_browser_info thy);
-
-val _ =
-  Theory.setup
-   (Theory.at_begin reset_browser_info #>
-    Browser_Info.put {chapter = Context.PureN, name = Context.PureN});
-
-
-
 (** global browser info state **)
 
 (* type browser_info *)
@@ -162,7 +137,8 @@
 
 fun theory_link (curr_chapter, curr_session) thy =
   let
-    val {chapter, name = session, ...} = Browser_Info.get thy;
+    val session = Resources.theory_qualifier (Context.theory_long_name thy);
+    val chapter = Resources.session_chapter session;
     val link = html_path (Context.theory_name thy);
   in
     if curr_session = session then SOME link
@@ -188,6 +164,6 @@
         if is_session_theory thy then
           add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name))
         else ();
-    in thy |> Browser_Info.put {chapter = chapter, name = session_name} end);
+    in thy end);
 
 end;
--- a/src/Pure/Thy/sessions.scala	Sun Nov 15 18:16:20 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Sun Nov 15 22:00:45 2020 +0100
@@ -811,6 +811,9 @@
           case entries => Some(name -> entries.map(_.info))
         })
 
+    def session_chapters: List[(String, String)] =
+      build_topological_order.map(name => name -> apply(name).chapter)
+
     override def toString: String =
       imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")")
   }
--- a/src/Pure/Tools/build.ML	Sun Nov 15 18:16:20 2020 +0100
+++ b/src/Pure/Tools/build.ML	Sun Nov 15 22:00:45 2020 +0100
@@ -89,8 +89,8 @@
         let
           val (symbol_codes, (command_timings, (verbose, (browser_info,
             (documents, (parent_name, (chapter, (session_name, (master_dir,
-            (theories, (session_positions, (session_directories, (doc_names, (global_theories,
-            (loaded_theories, bibtex_entries))))))))))))))) =
+            (theories, (session_positions, (session_directories, (session_chapters,
+            (doc_names, (global_theories, (loaded_theories, bibtex_entries)))))))))))))))) =
             YXML.parse_body args_yxml |>
               let
                 open XML.Decode;
@@ -102,9 +102,10 @@
                     (pair path
                       (pair (((list (pair Options.decode (list (pair string position))))))
                         (pair (list (pair string properties))
-                          (pair (list (pair string string)) (pair (list string)
+                          (pair (list (pair string string))
                             (pair (list (pair string string)) (pair (list string)
-                              (list (pair string (list string)))))))))))))))))
+                              (pair (list (pair string string)) (pair (list string)
+                                (list (pair string (list string))))))))))))))))))
               end;
 
           val symbols = HTML.make_symbols symbol_codes;
@@ -115,6 +116,7 @@
                 Resources.init_session
                   {session_positions = session_positions,
                    session_directories = session_directories,
+                   session_chapters = session_chapters,
                    bibtex_entries = bibtex_entries,
                    docs = doc_names,
                    global_theories = global_theories,
--- a/src/Pure/Tools/build.scala	Sun Nov 15 18:16:20 2020 +0100
+++ b/src/Pure/Tools/build.scala	Sun Nov 15 22:00:45 2020 +0100
@@ -180,15 +180,18 @@
                 pair(list(pair(Options.encode, list(pair(string, properties)))),
                 pair(list(pair(string, properties)),
                 pair(list(pair(string, string)),
-                pair(list(string), pair(list(pair(string, string)),
-                pair(list(string), list(pair(string, list(string))))))))))))))))))(
+                pair(list(pair(string, string)),
+                pair(list(string),
+                pair(list(pair(string, string)),
+                pair(list(string), list(pair(string, list(string)))))))))))))))))))(
               (Symbol.codes, (command_timings0, (verbose, (store.browser_info,
                 (documents, (parent, (info.chapter, (session_name, (Path.current,
                 (info.theories,
                 (sessions_structure.session_positions,
                 (sessions_structure.dest_session_directories,
+                (sessions_structure.session_chapters,
                 (base.doc_names, (base.global_theories.toList,
-                (base.loaded_theories.keys, sessions_structure.bibtex_entries))))))))))))))))
+                (base.loaded_theories.keys, sessions_structure.bibtex_entries)))))))))))))))))
             })
 
         val env =