disallow concurrent execution attempt explicitly -- it should never happen due to management of singleton execution;
tuned error messages: prefer plain "error" as in document.ML;
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) =