1.1 --- a/src/Pure/PIDE/command.ML	Fri Jul 12 12:17:03 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Jul 12 12:18:17 2013 +0200
     1.3 @@ -50,20 +50,18 @@
     1.4   | Result res => not (Exn.is_interrupt_exn res));
     1.5  
     1.6  fun memo_exec execution_id (Memo v) =
     1.7 -  (case Synchronized.value v of
     1.8 -    Result res => res
     1.9 -  | Expr _ =>
    1.10 -      Synchronized.timed_access v (fn _ => SOME Time.zeroTime)
    1.11 -        (fn Result res => SOME (res, Result res)
    1.12 -          | expr as Expr (exec_id, e) =>
    1.13 -              uninterruptible (fn restore_attributes => fn () =>
    1.14 -                if Execution.running execution_id exec_id then
    1.15 -                  let
    1.16 -                    val res = Exn.capture (restore_attributes e) ();
    1.17 -                    val _ = Execution.finished exec_id;
    1.18 -                  in SOME (res, Result res) end
    1.19 -                else SOME (Exn.interrupt_exn, expr)) ())
    1.20 -      |> (fn NONE => error "Concurrent execution attempt" | SOME res => res))
    1.21 +  Synchronized.guarded_access v
    1.22 +    (fn expr =>
    1.23 +      (case expr of
    1.24 +        Result res => SOME (res, expr)
    1.25 +      | Expr (exec_id, e) =>
    1.26 +          uninterruptible (fn restore_attributes => fn () =>
    1.27 +            if Execution.running execution_id exec_id then
    1.28 +              let
    1.29 +                val res = Exn.capture (restore_attributes e) ();
    1.30 +                val _ = Execution.finished exec_id;
    1.31 +              in SOME (res, Result res) end
    1.32 +            else SOME (Exn.interrupt_exn, expr)) ()))
    1.33    |> Exn.release |> ignore;
    1.34  
    1.35  fun memo_fork params execution_id (Memo v) =