# HG changeset patch
# User wenzelm
# Date 1598121451 -7200
# Node ID eef421b724c0589d87555d2f5ea00845fce8b645
# Parent  742d9401591886f1ab15caeb28fd0f6ec5951235
clarified names;

diff -r 742d94015918 -r eef421b724c0 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Sat Aug 22 20:32:44 2020 +0200
+++ b/src/Pure/System/scala.scala	Sat Aug 22 20:37:31 2020 +0200
@@ -116,16 +116,16 @@
         if (!ok && errors.isEmpty) List("Error") else errors
       }
     }
+  }
 
-    object Toplevel extends Fun("scala_toplevel")
+  object Toplevel extends Fun("scala_toplevel")
+  {
+    def apply(source: String): String =
     {
-      def apply(source: String): String =
-      {
-        val errors =
-          try { Compiler.context().toplevel(source) }
-          catch { case ERROR(msg) => List(msg) }
-        locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
-      }
+      val errors =
+        try { Compiler.context().toplevel(source) }
+        catch { case ERROR(msg) => List(msg) }
+      locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
     }
   }
 
@@ -221,5 +221,5 @@
 class Scala_Functions extends Scala.Functions(
   Scala.Echo,
   Scala.Sleep,
-  Scala.Compiler.Toplevel,
-  Bibtex.Check)
+  Scala.Toplevel,
+  Bibtex.Check_Database)
diff -r 742d94015918 -r eef421b724c0 src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML	Sat Aug 22 20:32:44 2020 +0200
+++ b/src/Pure/Thy/bibtex.ML	Sat Aug 22 20:37:31 2020 +0200
@@ -20,7 +20,7 @@
 type message = string * Position.T;
 
 fun check_database pos0 database =
-  \<^scala>\<open>check_bibtex_database\<close> database
+  \<^scala>\<open>bibtex_check_database\<close> database
   |> YXML.parse_body
   |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end
   |> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props pos0));
diff -r 742d94015918 -r eef421b724c0 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Sat Aug 22 20:32:44 2020 +0200
+++ b/src/Pure/Thy/bibtex.scala	Sat Aug 22 20:37:31 2020 +0200
@@ -145,7 +145,7 @@
     })
   }
 
-  object Check extends Scala.Fun("check_bibtex_database")
+  object Check_Database extends Scala.Fun("bibtex_check_database")
   {
     def apply(database: String): String =
     {