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