# HG changeset patch
# User wenzelm
# Date 1590264595 -7200
# Node ID a7b81dd9954effc98050aba63fe87419f9528c73
# Parent  b5191ededb6cf144d0efe5723e16578b96395013
tuned signature;

diff -r b5191ededb6c -r a7b81dd9954e src/Pure/System/scala.ML
--- a/src/Pure/System/scala.ML	Sat May 23 21:58:44 2020 +0200
+++ b/src/Pure/System/scala.ML	Sat May 23 22:09:55 2020 +0200
@@ -8,7 +8,6 @@
 sig
   val promise_function: string -> string -> string future
   val function: string -> string -> string
-  val function_yxml: string -> XML.body -> XML.body
   exception Null
   val check: string -> unit
 end;
@@ -42,8 +41,6 @@
 
 fun function name arg = Future.join (promise_function name arg);
 
-fun function_yxml name = YXML.string_of_body #> function name #> YXML.parse_body;
-
 
 (* fulfill *)
 
diff -r b5191ededb6c -r a7b81dd9954e src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Sat May 23 21:58:44 2020 +0200
+++ b/src/Pure/System/scala.scala	Sat May 23 22:09:55 2020 +0200
@@ -100,18 +100,7 @@
 
   /* registered functions */
 
-  object Fun
-  {
-    def apply(name: String, fn: String => String): Fun =
-      new Fun(name, fn, false)
-
-    def yxml(name: String, fn: XML.Body => XML.Body): Fun =
-      new Fun(name, s => YXML.string_of_body(fn(YXML.parse_body(s))), true)
-  }
-  class Fun private(val name: String, val fn: String => String, val yxml: Boolean)
-  {
-    def decl: (String, Boolean) = (name, yxml)
-  }
+  sealed case class Fun(name: String, apply: String => String)
 
   lazy val functions: List[Fun] =
     Isabelle_System.services.collect { case c: Isabelle_Scala_Functions => c.functions.toList }.flatten
@@ -125,9 +114,9 @@
   }
 
   def function(name: String, arg: String): (Tag.Value, String) =
-    functions.collectFirst({ case fun if fun.name == name => fun.fn }) match {
-      case Some(fn) =>
-        Exn.capture { fn(arg) } match {
+    functions.find(fun => fun.name == name) match {
+      case Some(fun) =>
+        Exn.capture { fun.apply(arg) } match {
           case Exn.Res(null) => (Tag.NULL, "")
           case Exn.Res(res) => (Tag.OK, res)
           case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "")
@@ -209,6 +198,5 @@
 
 class Functions extends Isabelle_Scala_Functions(
   Scala.Fun("echo", identity),
-  Scala.Fun.yxml("echo_yxml", identity),
   Scala.Fun("scala_check", Scala.check_yxml),
   Scala.Fun("check_bibtex_database", Bibtex.check_database_yxml))