src/Pure/System/scala.scala
changeset 77028 f5896dea6fce
parent 77027 ac7af931189f
child 78605 0bbbf8e26708
--- 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,