# HG changeset patch
# User wenzelm
# Date 1419706315 -3600
# Node ID e99f706aeab9fccb936f931d3aba77fe8d7428fb
# Parent  5a783837b50b62615ff3ea2278a894d62372ce66
memo_fork without locking, to avoid rare deadlock in Event_Timer.request due to execution overrun;

diff -r 5a783837b50b -r e99f706aeab9 src/Pure/PIDE/command.ML
--- 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))));