--- a/src/Pure/System/invoke_scala.ML Mon Jul 11 16:48:02 2011 +0200
+++ b/src/Pure/System/invoke_scala.ML Mon Jul 11 17:10:32 2011 +0200
@@ -8,14 +8,18 @@
signature INVOKE_SCALA =
sig
- val method: string -> string -> string future
exception Null
+ val method: string -> string -> string
+ val promise_method: string -> string -> string future
val fulfill_method: string -> string -> string -> unit
end;
structure Invoke_Scala: INVOKE_SCALA =
struct
+exception Null;
+
+
(* pending promises *)
val new_id = string_of_int o Synchronized.counter ();
@@ -26,7 +30,7 @@
(* method invocation *)
-fun method name arg =
+fun promise_method name arg =
let
val id = new_id ();
val promise = Future.promise () : string future;
@@ -34,11 +38,11 @@
val _ = Output.raw_message (Markup.invoke_scala name id) arg;
in promise end;
+fun method name arg = Future.join (promise_method name arg);
+
(* fulfill method *)
-exception Null;
-
fun fulfill_method id tag res =
let
val result =