changeset 71876 | ad063ac1f617 |
parent 71873 | a7b81dd9954e |
child 71881 | 71de0a253842 |
--- a/src/Pure/System/scala.ML Sun May 24 10:36:42 2020 +0200 +++ b/src/Pure/System/scala.ML Sun May 24 12:38:41 2020 +0200 @@ -32,6 +32,7 @@ fun promise_function name arg = let + val _ = if Resources.is_pide () then () else raise Fail "PIDE session required"; val id = new_id (); fun abort () = Output.protocol_message (Markup.cancel_scala id) []; val promise = Future.promise_name "invoke_scala" abort : string future;