src/Pure/PIDE/command.ML
changeset 53739 00170ef1dc39
parent 53737 75afb82daf5c
child 53741 ff2f0818aebc
     1.1 --- a/src/Pure/PIDE/command.ML	Thu Jul 11 16:35:37 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Thu Jul 11 18:41:05 2013 +0200
     1.3 @@ -54,10 +54,7 @@
     1.4                  let
     1.5                    val _ = Exec.running exec_id;
     1.6                    val res = Exn.capture (restore_attributes e) ();
     1.7 -                  val _ =
     1.8 -                    if Exn.is_interrupt_exn res
     1.9 -                    then Exec.canceled exec_id
    1.10 -                    else Exec.finished exec_id;
    1.11 +                  val _ = Exec.finished exec_id (not (Exn.is_interrupt_exn res));
    1.12                  in SOME (res, Result res) end) ())
    1.13        |> (fn NONE => error ("Concurrent execution attempt: " ^ Document_ID.print exec_id)
    1.14             | SOME res => res))