| changeset 52785 | ecc7d8de4f94 |
| parent 52784 | 4ba2e8b9972f |
| child 52850 | 9fff9f78240a |
--- a/src/Pure/PIDE/command.ML Tue Jul 30 11:38:43 2013 +0200 +++ b/src/Pure/PIDE/command.ML Tue Jul 30 11:44:06 2013 +0200 @@ -47,9 +47,7 @@ | Result res => Exn.release res); fun memo_finished (Memo v) = - (case Synchronized.value v of - Expr _ => false - | Result _ => true); + (case Synchronized.value v of Expr _ => false | Result _ => true); fun memo_exec execution_id (Memo v) = Synchronized.timed_access v (K (SOME Time.zeroTime))