src/Pure/System/invoke_scala.ML
changeset 70991 f9f7c34b7dd4
parent 66166 c88d1c36c9c3
equal deleted inserted replaced
70990:e5e34bd28257 70991:f9f7c34b7dd4
    31   let
    31   let
    32     val id = new_id ();
    32     val id = new_id ();
    33     fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
    33     fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
    34     val promise = Future.promise_name "invoke_scala" abort : string future;
    34     val promise = Future.promise_name "invoke_scala" abort : string future;
    35     val _ = Synchronized.change promises (Symtab.update (id, promise));
    35     val _ = Synchronized.change promises (Symtab.update (id, promise));
    36     val _ = Output.protocol_message (Markup.invoke_scala name id) [arg];
    36     val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg];
    37   in promise end;
    37   in promise end;
    38 
    38 
    39 fun method name arg = Future.join (promise_method name arg);
    39 fun method name arg = Future.join (promise_method name arg);
    40 
    40 
    41 
    41