changeset 53922 | ecc7d8de4f94 |
parent 53921 | 4ba2e8b9972f |
child 53987 | 9fff9f78240a |
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))