# HG changeset patch
# User wenzelm
# Date 1333629294 -7200
# Node ID ca5eb90cc84a8651a9b9dd6c071ad181a7e9965c
# Parent  b8aeab386414712eb3652317a2d33239dfbe5f2e
less ambitious memo_eval, since memo_result is still not robust here;

diff -r b8aeab386414 -r ca5eb90cc84a 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;