more direct check of bibtex entries via Isabelle/Scala;

--- a/src/Pure/PIDE/markup.ML	Fri Jan 20 16:30:09 2023 +0100
+++ b/src/Pure/PIDE/markup.ML	Fri Jan 20 19:52:52 2023 +0100
@@ -86,6 +86,7 @@
   val deleteN: string val delete: T
   val load_commandN: string
   val bash_functionN: string
+  val bibtex_entryN: string
   val scala_functionN: string
   val system_optionN: string
   val sessionN: string
@@ -489,6 +490,7 @@
 
 val load_commandN = "load_command";
 val bash_functionN = "bash_function";
+val bibtex_entryN = "bibtex_entry";
 val scala_functionN = "scala_function";
 val system_optionN = "system_option";
 

--- a/src/Pure/PIDE/resources.ML	Fri Jan 20 16:30:09 2023 +0100
+++ b/src/Pure/PIDE/resources.ML	Fri Jan 20 19:52:52 2023 +0100
@@ -10,7 +10,6 @@
   val init_session:
     {session_positions: (string * Properties.T) list,
      session_directories: (string * string) list,
-     bibtex_entries: (string * string list) list,
      command_timings: Properties.T list,
      load_commands: (string * Position.T) list,
      scala_functions: (string * ((bool * bool) * Position.T)) list,
@@ -30,7 +29,6 @@
   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}
@@ -105,7 +103,6 @@
 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,
     timings = empty_timings,
     load_commands = []: (string * Position.T) list,
     scala_functions = Symtab.empty: ((bool * bool) * Position.T) Symtab.table},
@@ -116,7 +113,7 @@
   Synchronized.var "Sessions.base" empty_session_base;
 
 fun init_session
-    {session_positions, session_directories, bibtex_entries, command_timings, load_commands,
+    {session_positions, session_directories, command_timings, load_commands,
       scala_functions, global_theories, loaded_theories} =
   Synchronized.change global_session_base
     (fn _ =>
@@ -124,7 +121,6 @@
         session_directories =
           Symtab.build (session_directories |> fold_rev (fn (dir, name) =>
             Symtab.cons_list (name, Path.explode dir))),
-        bibtex_entries = Symtab.make bibtex_entries,
         timings = make_timings command_timings,
         load_commands = load_commands,
         scala_functions = Symtab.make scala_functions},
@@ -133,22 +129,21 @@
 
 fun init_session_yxml yxml =
   let
-    val (session_positions, (session_directories, (bibtex_entries, (command_timings,
-        (load_commands, (scala_functions, (global_theories, loaded_theories))))))) =
+    val (session_positions, (session_directories, (command_timings,
+        (load_commands, (scala_functions, (global_theories, loaded_theories)))))) =
       YXML.parse_body_bytes yxml |>
         let open XML.Decode in
           (pair (list (pair string properties))
             (pair (list (pair string string))
-              (pair (list (pair string (list string))) (pair (list properties)
+              (pair (list properties)
                 (pair (list (pair string properties))
                   (pair (list (pair string (pair (pair bool bool) properties)))
-                    (pair (list (pair string string)) (list string))))))))
+                    (pair (list (pair string string)) (list string)))))))
         end;
   in
     init_session
       {session_positions = session_positions,
        session_directories = session_directories,
-       bibtex_entries = bibtex_entries,
        command_timings = command_timings,
        load_commands = (map o apsnd) Position.of_properties load_commands,
        scala_functions = (map o apsnd o apsnd) Position.of_properties scala_functions,
@@ -268,9 +263,6 @@
   if literal_theory theory then theory
   else Long_Name.qualify qualifier theory;
 
-fun theory_bibtex_entries theory =
-  Symtab.lookup_list (get_session_base1 #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/PIDE/resources.scala	Fri Jan 20 16:30:09 2023 +0100
+++ b/src/Pure/PIDE/resources.scala	Fri Jan 20 19:52:52 2023 +0100
@@ -43,19 +43,17 @@
     YXML.string_of_body(
       pair(list(pair(string, properties)),
       pair(list(pair(string, string)),
-      pair(list(pair(string, list(string))),
       pair(list(properties),
       pair(list(pair(string, properties)),
       pair(list(Scala.encode_fun),
-      pair(list(pair(string, string)), list(string))))))))(
+      pair(list(pair(string, string)), list(string)))))))(
        (sessions_structure.session_positions,
        (sessions_structure.dest_session_directories,
-       (sessions_structure.bibtex_entries,
        (command_timings,
        (Command_Span.load_commands.map(cmd => (cmd.name, cmd.position)),
        (Scala.functions,
        (sessions_structure.global_theories.toList,
-        session_base.loaded_theories.keys)))))))))
+        session_base.loaded_theories.keys))))))))
   }
 
 

--- a/src/Pure/System/scala.scala	Fri Jan 20 16:30:09 2023 +0100
+++ b/src/Pure/System/scala.scala	Fri Jan 20 19:52:52 2023 +0100
@@ -96,19 +96,6 @@
     }
   }
 
-  object Theory_Name extends Fun("command_theory_name") with Single_Fun {
-    val here = Scala_Project.here
-    override def invoke(session: Session, args: List[Bytes]): List[Bytes] = {
-      val id = Value.Long.parse(Library.the_single(args).text)
-      val name =
-        session.get_state().lookup_id(id) match {
-          case None => ""
-          case Some(st) => st.command.node_name.theory
-        }
-      List(Bytes(name))
-    }
-  }
-
 
 
   /** compiler **/
@@ -378,7 +365,6 @@
 class Scala_Functions extends Scala.Functions(
   Scala.Echo,
   Scala.Sleep,
-  Scala.Theory_Name,
   Scala.Toplevel,
   Scala_Build.Scala_Fun,
   Base64.Decode,
@@ -389,6 +375,7 @@
   Compress.Zstd_Uncompress,
   Doc.Doc_Names,
   Bibtex.Check_Database,
+  Bibtex.Session_Entries,
   Isabelle_System.Make_Directory,
   Isabelle_System.Copy_Dir,
   Isabelle_System.Copy_File,

--- a/src/Pure/Thy/bibtex.ML	Fri Jan 20 16:30:09 2023 +0100
+++ b/src/Pure/Thy/bibtex.ML	Fri Jan 20 19:52:52 2023 +0100
@@ -9,6 +9,7 @@
   val check_database:
     Position.T -> string -> (string * Position.T) list * (string * Position.T) list
   val check_database_output: Position.T -> string -> unit
+  val check_bibtex_entry: Proof.context -> string * Position.T -> unit
   val cite_macro: string Config.T
   val cite_antiquotation: binding -> (Proof.context -> string) -> theory -> theory
 end;
@@ -35,6 +36,29 @@
   end;
 
 
+(* check bibtex entry *)
+
+fun check_bibtex_entry ctxt (name, pos) =
+  let
+    fun warn () =
+      if Context_Position.is_visible ctxt then
+        warning ("Unknown session context: cannot check Bibtex entry " ^
+          quote name ^ Position.here pos)
+      else ();
+  in
+    if name = "*" then ()
+    else
+      (case Position.id_of pos of
+        NONE => warn ()
+      | SOME id =>
+          (case \<^scala>\<open>bibtex_session_entries\<close> [id] of
+            [] => warn ()
+          | _ :: entries =>
+              Completion.check_entity Markup.bibtex_entryN (map (rpair Position.none) entries)
+                ctxt (name, pos) |> ignore))
+  end;
+
+
 (* document antiquotations *)
 
 val cite_macro = Attrib.setup_config_string \<^binding>\<open>cite_macro\<close> (K "");
@@ -48,19 +72,6 @@
 
 val parse_citations = Parse.and_list1 Args.name_position;
 
-fun command_theory_name () =
-  let
-    fun err () = error ("Cannot determine command theory name: bad PIDE id");
-    val res =
-      (case Position.id_of (Position.thread_data ()) of
-        SOME id => \<^scala>\<open>command_theory_name\<close> id
-      | NONE => err ());
-  in if res = "" then err () else res end;
-
-fun theory_name thy =
-  let val name0 = Context.theory_long_name thy;
-  in if name0 = Context.PureN then command_theory_name () else name0 end;
-
 fun cite_command ctxt get_kind ((opt_loc, citations), macro_name) =
   let
     val loc = the_default Input.empty opt_loc;
@@ -68,15 +79,7 @@
       Context_Position.reports ctxt
         (Document_Output.document_reports loc @
           map (fn (name, pos) => (pos, Markup.citation name)) citations);
-
-    val thy_name = theory_name (Proof_Context.theory_of ctxt);
-    val bibtex_entries = Resources.theory_bibtex_entries thy_name;
-    val _ =
-      if null bibtex_entries andalso thy_name <> Context.PureN then ()
-      else
-        citations |> List.app (fn (name, pos) =>
-          if member (op =) bibtex_entries name orelse name = "*" then ()
-          else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos));
+    val _ = List.app (check_bibtex_entry ctxt) citations;
 
     val kind = if macro_name = "" then get_kind ctxt else macro_name;
     val location = Document_Output.output_document ctxt {markdown = false} loc;

--- a/src/Pure/Thy/bibtex.scala	Fri Jan 20 16:30:09 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Fri Jan 20 19:52:52 2023 +0100
@@ -210,6 +210,24 @@
       new Entries(entries ::: other.entries, errors ::: other.errors)
   }
 
+  object Session_Entries extends Scala.Fun("bibtex_session_entries") {
+    val here = Scala_Project.here
+
+    override def invoke(session: Session, args: List[Bytes]): List[Bytes] = {
+      val sessions = session.resources.sessions_structure
+      val id = Value.Long.parse(Library.the_single(args).text)
+      val qualifier =
+        session.get_state().lookup_id(id) match {
+          case None => Sessions.DRAFT
+          case Some(st) => sessions.theory_qualifier(st.command.node_name.theory)
+        }
+      val res =
+        if (qualifier == Sessions.DRAFT || !sessions.defined(qualifier)) Nil
+        else qualifier :: sessions(qualifier).bibtex_entries.entries.map(_.info)
+      res.map(Bytes.apply)
+    }
+  }
+
 
   /* completion */