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;
-