src/Pure/System/scala.ML
changeset 72103 7b318273a4aa
parent 71912 b9fbc93f3a24
child 72151 64df1e514005
equal deleted inserted replaced
72101:c65614b556b2 72103:7b318273a4aa
    31 
    31 
    32 (* invoke function *)
    32 (* invoke function *)
    33 
    33 
    34 fun promise_function name arg =
    34 fun promise_function name arg =
    35   let
    35   let
    36     val _ = if Resources.is_pide () then () else raise Fail "PIDE session required";
       
    37     val id = new_id ();
    36     val id = new_id ();
    38     fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
    37     fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
    39     val promise = Future.promise_name "invoke_scala" abort : string future;
    38     val promise = Future.promise_name "invoke_scala" abort : string future;
    40     val _ = Synchronized.change promises (Symtab.update (id, promise));
    39     val _ = Synchronized.change promises (Symtab.update (id, promise));
    41     val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg];
    40     val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg];