more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;

--- a/etc/settings	Sat May 23 12:04:24 2020 +0200
+++ b/etc/settings	Sat May 23 21:43:30 2020 +0200
@@ -23,6 +23,8 @@
 isabelle_scala_service 'isabelle.Tools'
 [ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_service 'isabelle.Admin_Tools'
 
+isabelle_scala_service 'isabelle.Functions'
+
 isabelle_scala_service 'isabelle.Bibtex$File_Format'
 
 #paranoia settings -- avoid intrusion of alien options

--- a/src/Pure/System/scala.ML	Sat May 23 12:04:24 2020 +0200
+++ b/src/Pure/System/scala.ML	Sat May 23 21:43:30 2020 +0200
@@ -6,15 +6,16 @@
 
 signature SCALA =
 sig
-  val method: string -> string -> string
-  val promise_method: string -> string -> string future
+  val promise_function: string -> string -> string future
+  val function: string -> string -> string
+  val function_yxml: string -> XML.body -> XML.body
   exception Null
 end;
 
 structure Scala: SCALA =
 struct
 
-(** invoke JVM method via Isabelle/Scala **)
+(** invoke Scala functions from ML **)
 
 val _ = Session.protocol_handler "isabelle.Scala";
 
@@ -27,9 +28,9 @@
   Synchronized.var "Scala.promises" (Symtab.empty: string future Symtab.table);
 
 
-(* method invocation *)
+(* invoke function *)
 
-fun promise_method name arg =
+fun promise_function name arg =
   let
     val id = new_id ();
     fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
@@ -38,7 +39,9 @@
     val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg];
   in promise end;
 
-fun method name arg = Future.join (promise_method name arg);
+fun function name arg = Future.join (promise_function name arg);
+
+fun function_yxml name = YXML.string_of_body #> function name #> YXML.parse_body;
 
 
 (* fulfill *)

--- a/src/Pure/System/scala.scala	Sat May 23 12:04:24 2020 +0200
+++ b/src/Pure/System/scala.scala	Sat May 23 21:43:30 2020 +0200
@@ -84,53 +84,44 @@
 
 
 
-  /** invoke JVM method via Isabelle/Scala **/
+  /** invoke Scala functions from ML **/
+
+  /* registered functions */
 
-  /* method reflection */
-
-  private val Ext = new Regex("(.*)\\.([^.]*)")
-  private val STRING = Class.forName("java.lang.String")
+  object Fun
+  {
+    def apply(name: String, fn: String => String): Fun =
+      new Fun(name, fn, false)
 
-  private def get_method(name: String): String => String =
-    name match {
-      case Ext(class_name, method_name) =>
-        val m =
-          try { Class.forName(class_name).getMethod(method_name, STRING) }
-          catch {
-            case _: ClassNotFoundException | _: NoSuchMethodException =>
-              error("No such method: " + quote(name))
-          }
-        if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
-        if (m.getReturnType != STRING) error("Bad method return type: " + m.toString)
+    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)
+  }
 
-        (arg: String) => {
-          try { m.invoke(null, arg).asInstanceOf[String] }
-          catch {
-            case e: InvocationTargetException if e.getCause != null =>
-              throw e.getCause
-          }
-        }
-      case _ => error("Malformed method name: " + quote(name))
-    }
+  lazy val functions: List[Fun] =
+    Isabelle_System.services.collect { case c: Isabelle_Scala_Functions => c.functions.toList }.flatten
 
 
-  /* method invocation */
+  /* invoke function */
 
   object Tag extends Enumeration
   {
     val NULL, OK, ERROR, FAIL, INTERRUPT = Value
   }
 
-  def method(name: String, arg: String): (Tag.Value, String) =
-    Exn.capture { get_method(name) } match {
-      case Exn.Res(f) =>
-        Exn.capture { f(arg) } match {
+  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 {
           case Exn.Res(null) => (Tag.NULL, "")
           case Exn.Res(res) => (Tag.OK, res)
           case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "")
           case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
         }
-      case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
+      case None => (Tag.FAIL, "Unknown Isabelle/Scala function: " + quote(name))
     }
 }
 
@@ -172,7 +163,7 @@
       case Markup.Invoke_Scala(name, id) =>
         futures += (id ->
           Future.fork {
-            val (tag, result) = Scala.method(name, msg.text)
+            val (tag, result) = Scala.function(name, msg.text)
             fulfill(id, tag, result)
           })
         true
@@ -198,3 +189,13 @@
       Markup.Invoke_Scala.name -> invoke_scala,
       Markup.Cancel_Scala.name -> cancel_scala)
 }
+
+
+/* registered functions */
+
+class Isabelle_Scala_Functions(val functions: Scala.Fun*) extends Isabelle_System.Service
+
+class Functions extends Isabelle_Scala_Functions(
+  Scala.Fun("echo", identity),
+  Scala.Fun.yxml("echo_yxml", identity),
+  Scala.Fun("check_bibtex_database", Bibtex.check_database_yxml))

--- a/src/Pure/Thy/bibtex.ML	Sat May 23 12:04:24 2020 +0200
+++ b/src/Pure/Thy/bibtex.ML	Sat May 23 21:43:30 2020 +0200
@@ -20,7 +20,7 @@
 type message = string * Position.T;
 
 fun check_database pos0 database =
-  Scala.method "isabelle.Bibtex.check_database_yxml" database
+  Scala.function "check_bibtex_database" 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));