src/Pure/PIDE/resources.ML

--- 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));