1.1 --- a/src/Pure/PIDE/command.ML	Mon Jul 29 16:01:05 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Mon Jul 29 16:52:04 2013 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4   | Result res => not (Exn.is_interrupt_exn res));
     1.5  
     1.6  fun memo_exec execution_id (Memo v) =
     1.7 -  Synchronized.guarded_access v
     1.8 +  Synchronized.timed_access v (K (SOME Time.zeroTime))
     1.9      (fn expr =>
    1.10        (case expr of
    1.11          Expr (exec_id, e) =>
    1.12 @@ -63,7 +63,9 @@
    1.13                in SOME (Exn.is_interrupt_exn res, Result res) end
    1.14              else SOME (true, expr)) ()
    1.15        | Result _ => SOME (false, expr)))
    1.16 -  |> (fn true => Exn.interrupt () | false => ());
    1.17 +  |> (fn SOME false => ()
    1.18 +       | SOME true => Exn.interrupt ()
    1.19 +       | NONE => error "Conflicting command execution");
    1.20  
    1.21  fun memo_fork params execution_id (Memo v) =
    1.22    (case Synchronized.value v of