tuned;
authorwenzelm
Tue, 30 Jul 2013 11:44:06 +0200
changeset 53922ecc7d8de4f94
parent 53921 4ba2e8b9972f
child 53923 9795ea654905
tuned;
src/Pure/PIDE/command.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Tue Jul 30 11:38:43 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Tue Jul 30 11:44:06 2013 +0200
     1.3 @@ -47,9 +47,7 @@
     1.4    | Result res => Exn.release res);
     1.5  
     1.6  fun memo_finished (Memo v) =
     1.7 -  (case Synchronized.value v of
     1.8 -   Expr _ => false
     1.9 - | Result _ => true);
    1.10 +  (case Synchronized.value v of Expr _ => false | Result _ => true);
    1.11  
    1.12  fun memo_exec execution_id (Memo v) =
    1.13    Synchronized.timed_access v (K (SOME Time.zeroTime))