# HG changeset patch
# User wenzelm
# Date 1598121164 -7200
# Node ID 742d9401591886f1ab15caeb28fd0f6ec5951235
# Parent  07635a1b6fd2325d0d57764f623e8f884ed13761
clarified signature;

diff -r 07635a1b6fd2 -r 742d94015918 etc/settings
--- a/etc/settings	Sat Aug 22 20:09:11 2020 +0200
+++ b/etc/settings	Sat Aug 22 20:32:44 2020 +0200
@@ -23,7 +23,7 @@
 isabelle_scala_service 'isabelle.Tools'
 [ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_service 'isabelle.Admin_Tools'
 
-isabelle_scala_service 'isabelle.Functions'
+isabelle_scala_service 'isabelle.Scala_Functions'
 
 isabelle_scala_service 'isabelle.Bibtex$File_Format'
 
diff -r 07635a1b6fd2 -r 742d94015918 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Sat Aug 22 20:09:11 2020 +0200
+++ b/src/Pure/System/scala.scala	Sat Aug 22 20:32:44 2020 +0200
@@ -15,21 +15,42 @@
 
 object Scala
 {
+  /** registered functions **/
+
+  abstract class Fun(val name: String) extends Function[String, String]
+  {
+    override def toString: String = name
+    def apply(arg: String): String
+  }
+
+  class Functions(val functions: Fun*) extends Isabelle_System.Service
+
+  lazy val functions: List[Fun] =
+    Isabelle_System.make_services(classOf[Functions]).flatMap(_.functions)
+
+
+
   /** demo functions **/
 
-  def echo(arg: String): String = arg
+  object Echo extends Fun("echo")
+  {
+    def apply(arg: String): String = arg
+  }
 
-  def sleep(seconds: String): String =
+  object Sleep extends Fun("sleep")
   {
-    val t =
-      seconds match {
-        case Value.Double(s) => Time.seconds(s)
-        case _ => error("Malformed argument: " + quote(seconds))
-      }
-    val t0 = Time.now()
-    t.sleep
-    val t1 = Time.now()
-    (t1 - t0).toString
+    def apply(seconds: String): String =
+    {
+      val t =
+        seconds match {
+          case Value.Double(s) => Time.seconds(s)
+          case _ => error("Malformed argument: " + quote(seconds))
+        }
+      val t0 = Time.now()
+      t.sleep
+      val t1 = Time.now()
+      (t1 - t0).toString
+    }
   }
 
 
@@ -95,31 +116,23 @@
         if (!ok && errors.isEmpty) List("Error") else errors
       }
     }
-  }
 
-  def toplevel_yxml(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)) }
+    object Toplevel extends Fun("scala_toplevel")
+    {
+      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)) }
+      }
+    }
   }
 
 
 
   /** invoke Scala functions from ML **/
 
-  /* registered functions */
-
-  sealed case class Fun(name: String, apply: String => String)
-  {
-    override def toString: String = name
-  }
-
-  lazy val functions: List[Fun] =
-    Isabelle_System.make_services(classOf[Isabelle_Scala_Functions]).flatMap(_.functions)
-
-
   /* invoke function */
 
   object Tag extends Enumeration
@@ -130,7 +143,7 @@
   def function(name: String, arg: String): (Tag.Value, String) =
     functions.find(fun => fun.name == name) match {
       case Some(fun) =>
-        Exn.capture { fun.apply(arg) } match {
+        Exn.capture { fun(arg) } match {
           case Exn.Res(null) => (Tag.NULL, "")
           case Exn.Res(res) => (Tag.OK, res)
           case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "")
@@ -205,13 +218,8 @@
   }
 }
 
-
-/* registered functions */
-
-class Isabelle_Scala_Functions(val functions: Scala.Fun*) extends Isabelle_System.Service
-
-class Functions extends Isabelle_Scala_Functions(
-  Scala.Fun("echo", Scala.echo),
-  Scala.Fun("sleep", Scala.sleep),
-  Scala.Fun("scala_toplevel", Scala.toplevel_yxml),
-  Scala.Fun("check_bibtex_database", Bibtex.check_database_yxml))
+class Scala_Functions extends Scala.Functions(
+  Scala.Echo,
+  Scala.Sleep,
+  Scala.Compiler.Toplevel,
+  Bibtex.Check)
diff -r 07635a1b6fd2 -r 742d94015918 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Sat Aug 22 20:09:11 2020 +0200
+++ b/src/Pure/Thy/bibtex.scala	Sat Aug 22 20:32:44 2020 +0200
@@ -145,11 +145,14 @@
     })
   }
 
-  def check_database_yxml(database: String): String =
+  object Check extends Scala.Fun("check_bibtex_database")
   {
-    import XML.Encode._
-    YXML.string_of_body(pair(list(pair(string, properties)), list(pair(string, properties)))(
-      check_database(database)))
+    def apply(database: String): String =
+    {
+      import XML.Encode._
+      YXML.string_of_body(pair(list(pair(string, properties)), list(pair(string, properties)))(
+        check_database(database)))
+    }
   }