equal
deleted
inserted
replaced
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]; |