support Session argument for Scala.Fun;
more robust check of citations within the Pure theory before the theory header;

--- a/src/Pure/System/isabelle_system.scala	Fri Jan 20 13:53:45 2023 +0100
+++ b/src/Pure/System/isabelle_system.scala	Fri Jan 20 16:30:09 2023 +0100
@@ -543,7 +543,7 @@
 
   object Download extends Scala.Fun("download", thread = true) {
     val here = Scala_Project.here
-    override def invoke(args: List[Bytes]): List[Bytes] =
+    override def invoke(session: Session, args: List[Bytes]): List[Bytes] =
       args.map(url => download(url.text).bytes)
   }
 

--- a/src/Pure/System/scala.scala	Fri Jan 20 13:53:45 2023 +0100
+++ b/src/Pure/System/scala.scala	Fri Jan 20 16:30:09 2023 +0100
@@ -34,7 +34,7 @@
     def bytes: Boolean = false
     def position: Properties.T = here.position
     def here: Scala_Project.Here
-    def invoke(args: List[Bytes]): List[Bytes]
+    def invoke(session: Session, args: List[Bytes]): List[Bytes]
   }
 
   trait Single_Fun extends Fun { override def single: Boolean = true }
@@ -42,7 +42,7 @@
 
   abstract class Fun_Strings(name: String, thread: Boolean = false)
   extends Fun(name, thread = thread) {
-    override def invoke(args: List[Bytes]): List[Bytes] =
+    override def invoke(session: Session, args: List[Bytes]): List[Bytes] =
       apply(args.map(_.text)).map(Bytes.apply)
     def apply(args: List[String]): List[String]
   }
@@ -56,7 +56,7 @@
 
   abstract class Fun_Bytes(name: String, thread: Boolean = false)
     extends Fun(name, thread = thread) with Single_Fun with Bytes_Fun {
-    override def invoke(args: List[Bytes]): List[Bytes] =
+    override def invoke(session: Session, args: List[Bytes]): List[Bytes] =
       List(apply(Library.the_single(args)))
     def apply(arg: Bytes): Bytes
   }
@@ -96,6 +96,19 @@
     }
   }
 
+  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 **/
@@ -285,10 +298,10 @@
       case None => false
     }
 
-  def function_body(name: String, args: List[Bytes]): (Tag.Value, List[Bytes]) =
+  def function_body(session: Session, name: String, args: List[Bytes]): (Tag.Value, List[Bytes]) =
     functions.find(fun => fun.name == name) match {
       case Some(fun) =>
-        Exn.capture { fun.invoke(args) } match {
+        Exn.capture { fun.invoke(session, args) } match {
           case Exn.Res(null) => (Tag.NULL, Nil)
           case Exn.Res(res) => (Tag.OK, res)
           case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, Nil)
@@ -329,7 +342,7 @@
       msg.properties match {
         case Markup.Invoke_Scala(name, id) =>
           def body(): Unit = {
-            val (tag, res) = Scala.function_body(name, msg.chunks)
+            val (tag, res) = Scala.function_body(session, name, msg.chunks)
             result(id, tag, res)
           }
           val future =
@@ -365,6 +378,7 @@
 class Scala_Functions extends Scala.Functions(
   Scala.Echo,
   Scala.Sleep,
+  Scala.Theory_Name,
   Scala.Toplevel,
   Scala_Build.Scala_Fun,
   Base64.Decode,

--- a/src/Pure/Thy/bibtex.ML	Fri Jan 20 13:53:45 2023 +0100
+++ b/src/Pure/Thy/bibtex.ML	Fri Jan 20 16:30:09 2023 +0100
@@ -48,6 +48,19 @@
 
 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;
@@ -56,18 +69,13 @@
         (Document_Output.document_reports loc @
           map (fn (name, pos) => (pos, Markup.citation name)) citations);
 
-    val thy_name = Context.theory_long_name (Proof_Context.theory_of ctxt);
+    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 if thy_name = Context.PureN then
-            (if Context_Position.is_visible ctxt then
-               warning ("Missing theory context --- unchecked Bibtex entry " ^
-                 quote name ^ Position.here pos)
-             else ())
           else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos));
 
     val kind = if macro_name = "" then get_kind ctxt else macro_name;

--- a/src/Pure/Tools/scala_build.scala	Fri Jan 20 13:53:45 2023 +0100
+++ b/src/Pure/Tools/scala_build.scala	Fri Jan 20 16:30:09 2023 +0100
@@ -104,7 +104,7 @@
 
   object Scala_Fun extends Scala.Fun("scala_build") with Scala.Bytes_Fun {
     val here = Scala_Project.here
-    def invoke(args: List[Bytes]): List[Bytes] =
+    def invoke(session: Session, args: List[Bytes]): List[Bytes] =
       args match {
         case List(dir) =>
           val result = build_result(Path.explode(dir.text))