1.1 --- a/src/Pure/PIDE/command.ML	Thu Jul 11 14:56:58 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Thu Jul 11 15:56:12 2013 +0200
     1.3 @@ -45,13 +45,13 @@
     1.4  fun memo_result (Memo v) =
     1.5    (case Synchronized.value v of
     1.6      Result res => Exn.release res
     1.7 -  | _ => raise Fail "Unfinished memo result");
     1.8 +  | Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id));
     1.9  
    1.10  fun memo_exec (Memo v) =
    1.11    (case Synchronized.value v of
    1.12      Result res => res
    1.13 -  | _ =>
    1.14 -      Synchronized.guarded_access v
    1.15 +  | Expr (exec_id, _) =>
    1.16 +      Synchronized.timed_access v (fn _ => SOME Time.zeroTime)
    1.17          (fn Result res => SOME (res, Result res)
    1.18            | Expr (exec_id, e) =>
    1.19                uninterruptible (fn restore_attributes => fn () =>
    1.20 @@ -62,7 +62,9 @@
    1.21                      if Exn.is_interrupt_exn res
    1.22                      then Exec.canceled exec_id
    1.23                      else Exec.finished exec_id;
    1.24 -                in SOME (res, Result res) end) ()))
    1.25 +                in SOME (res, Result res) end) ())
    1.26 +      |> (fn NONE => error ("Concurrent execution attempt: " ^ Document_ID.print exec_id)
    1.27 +           | SOME res => res))
    1.28    |> Exn.release;
    1.29  
    1.30  fun memo_fork params (Memo v) =