# HG changeset patch # User wenzelm # Date 1590263010 -7200 # Node ID 28def00726ca2e80239cc90b5af06d179ba806c3 # Parent 82abfda58667d10be00f40e214d8ae8e315009eb more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment; diff -r 82abfda58667 -r 28def00726ca etc/settings --- 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 diff -r 82abfda58667 -r 28def00726ca src/Pure/System/scala.ML --- 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 *) diff -r 82abfda58667 -r 28def00726ca src/Pure/System/scala.scala --- 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)) diff -r 82abfda58667 -r 28def00726ca src/Pure/Thy/bibtex.ML --- 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));