less ambitious memo_eval, since memo_result is still not robust here;
authorwenzelm
Thu, 05 Apr 2012 14:34:54 +0200
changeset 47344 ca5eb90cc84a
parent 47343 b8aeab386414
child 47345 193251980a73
less ambitious memo_eval, since memo_result is still not robust here;
src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Apr 05 14:14:51 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Apr 05 14:34:54 2012 +0200
@@ -400,7 +400,7 @@
             |> modify_init
             |> Toplevel.put_id exec_id'_string);
       val exec' = Command.memo (fn () =>
-        let val (st, _) = Command.memo_result (snd (snd command_exec));
+        let val (st, _) = Command.memo_eval (snd (snd command_exec));  (* FIXME memo_result !?! *)
         in Command.run_command (tr ()) st end);
       val command_exec' = (command_id', (exec_id', exec'));
     in SOME (command_exec' :: execs, command_exec', init') end;