# HG changeset patch
# User wenzelm
# Date 1590000343 -7200
# Node ID 265bbad3d6af8ea7e1c625721882c5f2ae5cd352
# Parent  3c7852327787150604dfe89b8555e2364bb66966
clarified modules;

diff -r 3c7852327787 -r 265bbad3d6af src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed May 20 15:00:25 2020 +0100
+++ b/src/Pure/ROOT.ML	Wed May 20 20:45:43 2020 +0200
@@ -327,7 +327,7 @@
 ML_file "System/command_line.ML";
 ML_file "System/message_channel.ML";
 ML_file "System/isabelle_process.ML";
-ML_file "System/invoke_scala.ML";
+ML_file "System/scala.ML";
 ML_file "Thy/bibtex.ML";
 ML_file "PIDE/protocol.ML";
 ML_file "General/output_primitives_virtual.ML";
diff -r 3c7852327787 -r 265bbad3d6af src/Pure/System/invoke_scala.ML
--- a/src/Pure/System/invoke_scala.ML	Wed May 20 15:00:25 2020 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(*  Title:      Pure/System/invoke_scala.ML
-    Author:     Makarius
-
-JVM method invocation service via Isabelle/Scala.
-*)
-
-signature INVOKE_SCALA =
-sig
-  val method: string -> string -> string
-  val promise_method: string -> string -> string future
-  exception Null
-end;
-
-structure Invoke_Scala: INVOKE_SCALA =
-struct
-
-val _ = Session.protocol_handler "isabelle.Invoke_Scala";
-
-
-(* pending promises *)
-
-val new_id = string_of_int o Counter.make ();
-
-val promises =
-  Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table);
-
-
-(* method invocation *)
-
-fun promise_method name arg =
-  let
-    val id = new_id ();
-    fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
-    val promise = Future.promise_name "invoke_scala" abort : string future;
-    val _ = Synchronized.change promises (Symtab.update (id, promise));
-    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);
-
-
-(* fulfill *)
-
-exception Null;
-
-fun fulfill id tag res =
-  let
-    val result =
-      (case tag of
-        "0" => Exn.Exn Null
-      | "1" => Exn.Res res
-      | "2" => Exn.Exn (ERROR res)
-      | "3" => Exn.Exn (Fail res)
-      | "4" => Exn.Exn Exn.Interrupt
-      | _ => raise Fail "Bad tag");
-    val promise =
-      Synchronized.change_result promises
-        (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab));
-    val _ = Future.fulfill_result promise result;
-  in () end;
-
-val _ =
-  Isabelle_Process.protocol_command "Invoke_Scala.fulfill"
-    (fn [id, tag, res] =>
-      fulfill id tag res
-        handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn);
-
-end;
-
diff -r 3c7852327787 -r 265bbad3d6af src/Pure/System/invoke_scala.scala
--- a/src/Pure/System/invoke_scala.scala	Wed May 20 15:00:25 2020 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,128 +0,0 @@
-/*  Title:      Pure/System/invoke_scala.scala
-    Author:     Makarius
-
-JVM method invocation service via Isabelle/Scala.
-*/
-
-package isabelle
-
-
-import java.lang.reflect.{Method, Modifier, InvocationTargetException}
-
-import scala.util.matching.Regex
-
-
-object Invoke_Scala
-{
-  /* method reflection */
-
-  private val Ext = new Regex("(.*)\\.([^.]*)")
-  private val STRING = Class.forName("java.lang.String")
-
-  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)
-
-        (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))
-    }
-
-
-  /* method invocation */
-
-  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 {
-          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))
-    }
-}
-
-
-/* protocol handler */
-
-class Invoke_Scala extends Session.Protocol_Handler
-{
-  private var session: Session = null
-  private var futures = Map.empty[String, Future[Unit]]
-
-  override def init(init_session: Session): Unit =
-    synchronized { session = init_session }
-
-  override def exit(): Unit = synchronized
-  {
-    for ((id, future) <- futures) cancel(id, future)
-    futures = Map.empty
-  }
-
-  private def fulfill(id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
-    synchronized
-    {
-      if (futures.isDefinedAt(id)) {
-        session.protocol_command("Invoke_Scala.fulfill", id, tag.id.toString, res)
-        futures -= id
-      }
-    }
-
-  private def cancel(id: String, future: Future[Unit])
-  {
-    future.cancel
-    fulfill(id, Invoke_Scala.Tag.INTERRUPT, "")
-  }
-
-  private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
-  {
-    msg.properties match {
-      case Markup.Invoke_Scala(name, id) =>
-        futures += (id ->
-          Future.fork {
-            val (tag, result) = Invoke_Scala.method(name, msg.text)
-            fulfill(id, tag, result)
-          })
-        true
-      case _ => false
-    }
-  }
-
-  private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized
-  {
-    msg.properties match {
-      case Markup.Cancel_Scala(id) =>
-        futures.get(id) match {
-          case Some(future) => cancel(id, future)
-          case None =>
-        }
-        true
-      case _ => false
-    }
-  }
-
-  val functions =
-    List(
-      Markup.Invoke_Scala.name -> invoke_scala,
-      Markup.Cancel_Scala.name -> cancel_scala)
-}
diff -r 3c7852327787 -r 265bbad3d6af src/Pure/System/scala.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/scala.ML	Wed May 20 20:45:43 2020 +0200
@@ -0,0 +1,70 @@
+(*  Title:      Pure/System/scala.ML
+    Author:     Makarius
+
+Support for Scala at runtime.
+*)
+
+signature SCALA =
+sig
+  val method: string -> string -> string
+  val promise_method: string -> string -> string future
+  exception Null
+end;
+
+structure Scala: SCALA =
+struct
+
+(** invoke JVM method via Isabelle/Scala **)
+
+val _ = Session.protocol_handler "isabelle.Scala";
+
+
+(* pending promises *)
+
+val new_id = string_of_int o Counter.make ();
+
+val promises =
+  Synchronized.var "Scala.promises" (Symtab.empty: string future Symtab.table);
+
+
+(* method invocation *)
+
+fun promise_method name arg =
+  let
+    val id = new_id ();
+    fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
+    val promise = Future.promise_name "invoke_scala" abort : string future;
+    val _ = Synchronized.change promises (Symtab.update (id, promise));
+    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);
+
+
+(* fulfill *)
+
+exception Null;
+
+fun fulfill id tag res =
+  let
+    val result =
+      (case tag of
+        "0" => Exn.Exn Null
+      | "1" => Exn.Res res
+      | "2" => Exn.Exn (ERROR res)
+      | "3" => Exn.Exn (Fail res)
+      | "4" => Exn.Exn Exn.Interrupt
+      | _ => raise Fail "Bad tag");
+    val promise =
+      Synchronized.change_result promises
+        (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab));
+    val _ = Future.fulfill_result promise result;
+  in () end;
+
+val _ =
+  Isabelle_Process.protocol_command "Scala.fulfill"
+    (fn [id, tag, res] =>
+      fulfill id tag res
+        handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn);
+
+end;
diff -r 3c7852327787 -r 265bbad3d6af src/Pure/System/scala.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/scala.scala	Wed May 20 20:45:43 2020 +0200
@@ -0,0 +1,130 @@
+/*  Title:      Pure/System/scala.scala
+    Author:     Makarius
+
+Support for Scala at runtime.
+*/
+
+package isabelle
+
+
+import java.lang.reflect.{Method, Modifier, InvocationTargetException}
+
+import scala.util.matching.Regex
+
+
+object Scala
+{
+  /** invoke JVM method via Isabelle/Scala **/
+
+  /* method reflection */
+
+  private val Ext = new Regex("(.*)\\.([^.]*)")
+  private val STRING = Class.forName("java.lang.String")
+
+  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)
+
+        (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))
+    }
+
+
+  /* method invocation */
+
+  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 {
+          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))
+    }
+}
+
+
+/* protocol handler */
+
+class Scala extends Session.Protocol_Handler
+{
+  private var session: Session = null
+  private var futures = Map.empty[String, Future[Unit]]
+
+  override def init(init_session: Session): Unit =
+    synchronized { session = init_session }
+
+  override def exit(): Unit = synchronized
+  {
+    for ((id, future) <- futures) cancel(id, future)
+    futures = Map.empty
+  }
+
+  private def fulfill(id: String, tag: Scala.Tag.Value, res: String): Unit =
+    synchronized
+    {
+      if (futures.isDefinedAt(id)) {
+        session.protocol_command("Scala.fulfill", id, tag.id.toString, res)
+        futures -= id
+      }
+    }
+
+  private def cancel(id: String, future: Future[Unit])
+  {
+    future.cancel
+    fulfill(id, Scala.Tag.INTERRUPT, "")
+  }
+
+  private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
+  {
+    msg.properties match {
+      case Markup.Invoke_Scala(name, id) =>
+        futures += (id ->
+          Future.fork {
+            val (tag, result) = Scala.method(name, msg.text)
+            fulfill(id, tag, result)
+          })
+        true
+      case _ => false
+    }
+  }
+
+  private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized
+  {
+    msg.properties match {
+      case Markup.Cancel_Scala(id) =>
+        futures.get(id) match {
+          case Some(future) => cancel(id, future)
+          case None =>
+        }
+        true
+      case _ => false
+    }
+  }
+
+  val functions =
+    List(
+      Markup.Invoke_Scala.name -> invoke_scala,
+      Markup.Cancel_Scala.name -> cancel_scala)
+}
diff -r 3c7852327787 -r 265bbad3d6af src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML	Wed May 20 15:00:25 2020 +0100
+++ b/src/Pure/Thy/bibtex.ML	Wed May 20 20:45:43 2020 +0200
@@ -20,7 +20,7 @@
 type message = string * Position.T;
 
 fun check_database pos0 database =
-  Invoke_Scala.method "isabelle.Bibtex.check_database_yxml" database
+  Scala.method "isabelle.Bibtex.check_database_yxml" 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 3c7852327787 -r 265bbad3d6af src/Pure/build-jars
--- a/src/Pure/build-jars	Wed May 20 15:00:25 2020 +0100
+++ b/src/Pure/build-jars	Wed May 20 20:45:43 2020 +0200
@@ -120,7 +120,6 @@
   src/Pure/System/cygwin.scala
   src/Pure/System/distribution.scala
   src/Pure/System/getopts.scala
-  src/Pure/System/invoke_scala.scala
   src/Pure/System/isabelle_charset.scala
   src/Pure/System/isabelle_fonts.scala
   src/Pure/System/isabelle_process.scala
@@ -133,6 +132,7 @@
   src/Pure/System/posix_interrupt.scala
   src/Pure/System/process_result.scala
   src/Pure/System/progress.scala
+  src/Pure/System/scala.scala
   src/Pure/System/system_channel.scala
   src/Pure/System/tty_loop.scala
   src/Pure/Thy/bibtex.scala