clarified bibtex_entries: refer to overall session structure;

--- a/src/Pure/ML/ml_process.scala	Sat Nov 14 17:29:37 2020 +0100
+++ b/src/Pure/ML/ml_process.scala	Sun Nov 15 17:34:19 2020 +0100
@@ -91,10 +91,15 @@
           def print_sessions(list: List[(String, Position.T)]): String =
             ML_Syntax.print_list(
               ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
+          def print_bibtex_entries(list: List[(String, List[String])]): String =
+            ML_Syntax.print_list(
+              ML_Syntax.print_pair(ML_Syntax.print_string_bytes,
+                ML_Syntax.print_list(ML_Syntax.print_string_bytes)))(list)
 
           List("Resources.init_session" +
             "{session_positions = " + print_sessions(sessions_structure.session_positions) +
             ", session_directories = " + print_table(sessions_structure.dest_session_directories) +
+            ", bibtex_entries = " + print_bibtex_entries(sessions_structure.bibtex_entries) +
             ", docs = " + print_list(base.doc_names) +
             ", global_theories = " + print_table(base.global_theories.toList) +
             ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}")

--- a/src/Pure/PIDE/protocol.ML	Sat Nov 14 17:29:37 2020 +0100
+++ b/src/Pure/PIDE/protocol.ML	Sun Nov 15 17:34:19 2020 +0100
@@ -25,17 +25,20 @@
 
 val _ =
   Isabelle_Process.protocol_command "Prover.init_session"
-    (fn [session_positions_yxml, session_directories_yxml, doc_names_yxml, global_theories_yxml,
-          loaded_theories_yxml] =>
+    (fn [session_positions_yxml, session_directories_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;
         val decode_sessions =
           YXML.parse_body #> let open XML.Decode in list (pair string properties) end;
+        val decode_bibtex_entries =
+          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,
            session_directories = decode_table session_directories_yxml,
+           bibtex_entries = decode_bibtex_entries bibtex_entries_yxml,
            docs = decode_list doc_names_yxml,
            global_theories = decode_table global_theories_yxml,
            loaded_theories = decode_list loaded_theories_yxml}

--- a/src/Pure/PIDE/protocol.scala	Sat Nov 14 17:29:37 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala	Sun Nov 15 17:34:19 2020 +0100
@@ -303,11 +303,18 @@
     Symbol.encode_yxml(list(pair(string, properties))(lst))
   }
 
+  private def encode_bibtex_entries(lst: List[(String, List[String])]): String =
+  {
+    import XML.Encode._
+    Symbol.encode_yxml(list(pair(string, list(string)))(lst))
+  }
+
   def init_session(resources: Resources)
   {
     protocol_command("Prover.init_session",
       encode_sessions(resources.sessions_structure.session_positions),
       encode_table(resources.sessions_structure.dest_session_directories),
+      encode_bibtex_entries(resources.sessions_structure.bibtex_entries),
       encode_list(resources.session_base.doc_names),
       encode_table(resources.session_base.global_theories.toList),
       encode_list(resources.session_base.loaded_theories.keys))

--- a/src/Pure/PIDE/resources.ML	Sat Nov 14 17:29:37 2020 +0100
+++ b/src/Pure/PIDE/resources.ML	Sun Nov 15 17:34:19 2020 +0100
@@ -10,6 +10,7 @@
   val init_session:
     {session_positions: (string * Properties.T) list,
      session_directories: (string * string) list,
+     bibtex_entries: (string * string list) list,
      docs: string list,
      global_theories: (string * string) list,
      loaded_theories: string list} -> unit
@@ -23,6 +24,7 @@
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   val thy_path: Path.T -> Path.T
   val theory_qualifier: string -> string
+  val theory_bibtex_entries: string -> string list
   val find_theory_file: string -> Path.T option
   val import_name: string -> Path.T -> string ->
     {node_name: Path.T, master_dir: Path.T, theory_name: string}
@@ -54,6 +56,7 @@
 val empty_session_base =
   {session_positions = []: (string * entry) list,
    session_directories = Symtab.empty: Path.T list Symtab.table,
+   bibtex_entries = Symtab.empty: string list Symtab.table,
    docs = []: (string * entry) list,
    global_theories = Symtab.empty: string Symtab.table,
    loaded_theories = Symtab.empty: unit Symtab.table};
@@ -62,13 +65,15 @@
   Synchronized.var "Sessions.base" empty_session_base;
 
 fun init_session
-    {session_positions, session_directories, docs, global_theories, loaded_theories} =
+    {session_positions, session_directories, 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,
+       bibtex_entries = Symtab.make bibtex_entries,
        docs = sort_by #1 (map (apsnd make_entry o rpair []) docs),
        global_theories = Symtab.make global_theories,
        loaded_theories = Symtab.make_set loaded_theories});
@@ -78,6 +83,7 @@
     (fn {global_theories, loaded_theories, ...} =>
       {session_positions = [],
        session_directories = Symtab.empty,
+       bibtex_entries = Symtab.empty,
        docs = [],
        global_theories = global_theories,
        loaded_theories = loaded_theories});
@@ -148,6 +154,9 @@
   then theory
   else Long_Name.qualify qualifier theory;
 
+fun theory_bibtex_entries theory =
+  Symtab.lookup_list (get_session_base #bibtex_entries) (theory_qualifier theory);
+
 fun find_theory_file thy_name =
   let
     val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name));

--- a/src/Pure/Thy/bibtex.ML	Sat Nov 14 17:29:37 2020 +0100
+++ b/src/Pure/Thy/bibtex.ML	Sun Nov 15 17:34:19 2020 +0100
@@ -47,7 +47,7 @@
       (fn ctxt => fn (opt, citations) =>
         let
           val thy = Proof_Context.theory_of ctxt;
-          val bibtex_entries = Present.get_bibtex_entries thy;
+          val bibtex_entries = Resources.theory_bibtex_entries (Context.theory_long_name thy);
           val _ =
             if null bibtex_entries andalso Context.theory_name thy <> Context.PureN then ()
             else

--- a/src/Pure/Thy/present.ML	Sat Nov 14 17:29:37 2020 +0100
+++ b/src/Pure/Thy/present.ML	Sun Nov 15 17:34:19 2020 +0100
@@ -6,11 +6,10 @@
 
 signature PRESENT =
 sig
-  val get_bibtex_entries: theory -> string list
   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: string list -> int -> (unit -> HTML.text) -> theory -> theory
+  val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
 end;
 
 structure Present: PRESENT =
@@ -32,8 +31,8 @@
 
 (** theory data **)
 
-type browser_info = {chapter: string, name: string, bibtex_entries: string list};
-val empty_browser_info: browser_info = {chapter = "Unsorted", name = "Unknown", bibtex_entries = []};
+type browser_info = {chapter: string, name: string};
+val empty_browser_info: browser_info = {chapter = "Unsorted", name = "Unknown"};
 
 structure Browser_Info = Theory_Data
 (
@@ -50,9 +49,7 @@
 val _ =
   Theory.setup
    (Theory.at_begin reset_browser_info #>
-    Browser_Info.put {chapter = Context.PureN, name = Context.PureN, bibtex_entries = []});
-
-val get_bibtex_entries = #bibtex_entries o Browser_Info.get;
+    Browser_Info.put {chapter = Context.PureN, name = Context.PureN});
 
 
 
@@ -175,7 +172,7 @@
     else SOME (Path.parent + Path.parent + Path.basic chapter + Path.basic session + link)
   end;
 
-fun begin_theory bibtex_entries update_time mk_text thy =
+fun begin_theory update_time mk_text thy =
   with_session_info thy (fn {symbols, name = session_name, chapter, ...} =>
     let
       val name = Context.theory_name thy;
@@ -187,14 +184,10 @@
 
       val _ = update_html name (HTML.theory symbols name parent_specs (mk_text ()));
 
-      val bibtex_entries' =
+      val _ =
         if is_session_theory thy then
-          (add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name));
-           bibtex_entries)
-        else [];
-    in
-      thy
-      |> Browser_Info.put {chapter = chapter, name = session_name, bibtex_entries = bibtex_entries'}
-    end);
+          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);
 
 end;

--- a/src/Pure/Thy/sessions.scala	Sat Nov 14 17:29:37 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Sun Nov 15 17:34:19 2020 +0100
@@ -511,7 +511,7 @@
         case s => Some(dir + Path.explode(s))
       }
 
-    def bibtex_entries: List[Text.Info[String]] =
+    lazy val bibtex_entries: List[Text.Info[String]] =
       (for {
         (document_dir, file) <- document_files.iterator
         if Bibtex.is_bibtex(file.file_name)
@@ -804,6 +804,13 @@
     def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds_rev(ss)
     def imports_topological_order: List[String] = imports_graph.topological_order
 
+    def bibtex_entries: List[(String, List[String])] =
+      build_topological_order.flatMap(name =>
+        apply(name).bibtex_entries match {
+          case Nil => None
+          case entries => Some(name -> entries.map(_.info))
+        })
+
     override def toString: String =
       imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")")
   }

--- a/src/Pure/Thy/thy_info.ML	Sat Nov 14 17:29:37 2020 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sun Nov 15 17:34:19 2020 +0100
@@ -21,7 +21,6 @@
   type context =
     {options: Options.T,
      symbols: HTML.symbols,
-     bibtex_entries: string list,
      last_timing: Toplevel.transition -> Time.time}
   val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit
   val use_thy: string -> unit
@@ -187,13 +186,11 @@
 type context =
   {options: Options.T,
    symbols: HTML.symbols,
-   bibtex_entries: string list,
    last_timing: Toplevel.transition -> Time.time};
 
 fun default_context (): context =
   {options = Options.default (),
    symbols = HTML.no_symbols,
-   bibtex_entries = [],
    last_timing = K Time.zeroTime};
 
 
@@ -303,7 +300,7 @@
 
 fun eval_thy (context: context) update_time master_dir header text_pos text parents =
   let
-    val {options, symbols, bibtex_entries, last_timing} = context;
+    val {options, symbols, last_timing} = context;
     val (name, _) = #name header;
     val keywords =
       fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
@@ -314,7 +311,7 @@
 
     fun init () =
       Resources.begin_theory master_dir header parents
-      |> Present.begin_theory bibtex_entries update_time
+      |> Present.begin_theory update_time
         (fn () => implode (map (HTML.present_span symbols keywords) spans));
 
     val (results, thy) =

--- a/src/Pure/Tools/build.ML	Sat Nov 14 17:29:37 2020 +0100
+++ b/src/Pure/Tools/build.ML	Sun Nov 15 17:34:19 2020 +0100
@@ -55,11 +55,10 @@
 
 (* build theories *)
 
-fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) =
+fun build_theories symbols last_timing qualifier master_dir (options, thys) =
   let
     val context =
-      {options = options, symbols = symbols, bibtex_entries = bibtex_entries,
-        last_timing = last_timing};
+      {options = options, symbols = symbols, last_timing = last_timing};
     val condition = space_explode "," (Options.string options "condition");
     val conds = filter_out (can getenv_strict) condition;
   in
@@ -104,7 +103,8 @@
                       (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 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 +115,7 @@
                 Resources.init_session
                   {session_positions = session_positions,
                    session_directories = session_directories,
+                   bibtex_entries = bibtex_entries,
                    docs = doc_names,
                    global_theories = global_theories,
                    loaded_theories = loaded_theories};
@@ -133,8 +134,7 @@
 
               val res1 =
                 theories |>
-                  (List.app
-                      (build_theories symbols bibtex_entries last_timing session_name master_dir)
+                  (List.app (build_theories symbols last_timing session_name master_dir)
                     |> session_timing
                     |> Exn.capture);
               val res2 = Exn.capture Session.finish ();

--- a/src/Pure/Tools/build.scala	Sat Nov 14 17:29:37 2020 +0100
+++ b/src/Pure/Tools/build.scala	Sun Nov 15 17:34:19 2020 +0100
@@ -181,14 +181,14 @@
                 pair(list(pair(string, properties)),
                 pair(list(pair(string, string)),
                 pair(list(string), pair(list(pair(string, string)),
-                pair(list(string), list(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,
                 (base.doc_names, (base.global_theories.toList,
-                (base.loaded_theories.keys, info.bibtex_entries.map(_.info)))))))))))))))))
+                (base.loaded_theories.keys, sessions_structure.bibtex_entries))))))))))))))))
             })
 
         val env =