changeset 59188 | e99f706aeab9 |
parent 59123 | e68e44836d04 |
child 59193 | 59f1591a11cb |
--- a/src/Pure/PIDE/command.ML Wed Dec 24 10:06:37 2014 +0100 +++ b/src/Pure/PIDE/command.ML Sat Dec 27 19:51:55 2014 +0100 @@ -77,7 +77,7 @@ |> (fn NONE => error "Conflicting command execution" | _ => ()); fun memo_fork params execution_id (Memo v) = - (case Synchronized.value v of + (case Synchronized.peek v of Result _ => () | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec execution_id (Memo v))));