src/Pure/PIDE/command.ML
changeset 52602 00170ef1dc39
parent 52600 75afb82daf5c
child 52604 ff2f0818aebc
equal deleted inserted replaced
52601:55e62a25a7ce 52602:00170ef1dc39
    52           | Expr (exec_id, e) =>
    52           | Expr (exec_id, e) =>
    53               uninterruptible (fn restore_attributes => fn () =>
    53               uninterruptible (fn restore_attributes => fn () =>
    54                 let
    54                 let
    55                   val _ = Exec.running exec_id;
    55                   val _ = Exec.running exec_id;
    56                   val res = Exn.capture (restore_attributes e) ();
    56                   val res = Exn.capture (restore_attributes e) ();
    57                   val _ =
    57                   val _ = Exec.finished exec_id (not (Exn.is_interrupt_exn res));
    58                     if Exn.is_interrupt_exn res
       
    59                     then Exec.canceled exec_id
       
    60                     else Exec.finished exec_id;
       
    61                 in SOME (res, Result res) end) ())
    58                 in SOME (res, Result res) end) ())
    62       |> (fn NONE => error ("Concurrent execution attempt: " ^ Document_ID.print exec_id)
    59       |> (fn NONE => error ("Concurrent execution attempt: " ^ Document_ID.print exec_id)
    63            | SOME res => res))
    60            | SOME res => res))
    64   |> Exn.release;
    61   |> Exn.release;
    65 
    62