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;