# HG changeset patch
# User wenzelm
# Date 1310397032 -7200
# Node ID 5ca34f21cb4451794381e8942e04722edf192129
# Parent  c70bd78ec83c38488b0702230f7753e778921c06
tuned signature;

diff -r c70bd78ec83c -r 5ca34f21cb44 src/Pure/System/invoke_scala.ML
--- 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 =