# HG changeset patch
# User wenzelm
# Date 1373877732 -7200
# Node ID 42c14dba1daa4161aaf16ffef5973f10afbddf6c
# Parent  9437f440ef3f6d04054daa3179ae42127b8e2291
tuned;

diff -r 9437f440ef3f -r 42c14dba1daa src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Jul 15 10:31:41 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Mon Jul 15 10:42:12 2013 +0200
@@ -59,16 +59,16 @@
   Synchronized.guarded_access v
     (fn expr =>
       (case expr of
-        Result res => SOME (res, expr)
-      | Expr (exec_id, e) =>
+        Expr (exec_id, e) =>
           uninterruptible (fn restore_attributes => fn () =>
             if Execution.running execution_id exec_id then
               let
                 val res = Exn.capture (restore_attributes e) ();
                 val _ = Execution.finished exec_id;
-              in SOME (res, Result res) end
-            else SOME (Exn.interrupt_exn, expr)) ()))
-  |> Exn.release |> ignore;
+              in SOME (Exn.is_interrupt_exn res, Result res) end
+            else SOME (true, expr)) ()
+      | Result _ => SOME (false, expr)))
+  |> (fn true => Exn.interrupt () | false => ());
 
 fun memo_fork params execution_id (Memo v) =
   (case Synchronized.value v of