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