1.1 --- a/src/Pure/PIDE/command.ML	Mon Jul 15 10:31:41 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Mon Jul 15 10:42:12 2013 +0200
     1.3 @@ -59,16 +59,16 @@
     1.4    Synchronized.guarded_access v
     1.5      (fn expr =>
     1.6        (case expr of
     1.7 -        Result res => SOME (res, expr)
     1.8 -      | Expr (exec_id, e) =>
     1.9 +        Expr (exec_id, e) =>
    1.10            uninterruptible (fn restore_attributes => fn () =>
    1.11              if Execution.running execution_id exec_id then
    1.12                let
    1.13                  val res = Exn.capture (restore_attributes e) ();
    1.14                  val _ = Execution.finished exec_id;
    1.15 -              in SOME (res, Result res) end
    1.16 -            else SOME (Exn.interrupt_exn, expr)) ()))
    1.17 -  |> Exn.release |> ignore;
    1.18 +              in SOME (Exn.is_interrupt_exn res, Result res) end
    1.19 +            else SOME (true, expr)) ()
    1.20 +      | Result _ => SOME (false, expr)))
    1.21 +  |> (fn true => Exn.interrupt () | false => ());
    1.22  
    1.23  fun memo_fork params execution_id (Memo v) =
    1.24    (case Synchronized.value v of