changeset 72103 | 7b318273a4aa |
parent 71912 | b9fbc93f3a24 |
child 72151 | 64df1e514005 |
--- a/src/Pure/System/scala.ML Thu Aug 06 17:51:37 2020 +0200 +++ b/src/Pure/System/scala.ML Thu Aug 06 22:43:40 2020 +0200 @@ -33,7 +33,6 @@ 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;