# HG changeset patch
# User wenzelm
# Date 1373550972 -7200
# Node ID cad097fb46deceae4c5bf7cab60721f2419f9e1b
# Parent  a8a81453833d453ef5a8adfbe4de007d58025203
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;

diff -r a8a81453833d -r cad097fb46de src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Jul 11 14:56:58 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Thu Jul 11 15:56:12 2013 +0200
@@ -45,13 +45,13 @@
 fun memo_result (Memo v) =
   (case Synchronized.value v of
     Result res => Exn.release res
-  | _ => raise Fail "Unfinished memo result");
+  | Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id));
 
 fun memo_exec (Memo v) =
   (case Synchronized.value v of
     Result res => res
-  | _ =>
-      Synchronized.guarded_access v
+  | Expr (exec_id, _) =>
+      Synchronized.timed_access v (fn _ => SOME Time.zeroTime)
         (fn Result res => SOME (res, Result res)
           | Expr (exec_id, e) =>
               uninterruptible (fn restore_attributes => fn () =>
@@ -62,7 +62,9 @@
                     if Exn.is_interrupt_exn res
                     then Exec.canceled exec_id
                     else Exec.finished exec_id;
-                in SOME (res, Result res) end) ()))
+                in SOME (res, Result res) end) ())
+      |> (fn NONE => error ("Concurrent execution attempt: " ^ Document_ID.print exec_id)
+           | SOME res => res))
   |> Exn.release;
 
 fun memo_fork params (Memo v) =