tuned;
authorwenzelm
Wed Jul 03 21:32:58 2013 +0200 (2013-07-03 ago)
changeset 52512c4891dbd5161
parent 52511 d5d2093ff224
child 52513 04210c1bcb90
tuned;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Jul 03 17:50:47 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Jul 03 21:32:58 2013 +0200
     1.3 @@ -459,9 +459,9 @@
     1.4        val exec' =
     1.5          Command.memo (fn () =>
     1.6            let
     1.7 -            val (st, _) = Command.memo_result (snd (snd command_exec));
     1.8 +            val (st_malformed, _) = Command.memo_result (snd (snd command_exec));
     1.9              val tr = read ();
    1.10 -            val ({failed}, (st', malformed')) = Command.eval span tr st;
    1.11 +            val ({failed}, (st', malformed')) = Command.eval span tr st_malformed;
    1.12              val print = if failed then [] else Command.print tr st';
    1.13            in ((st', malformed'), print) end);
    1.14        val command_exec' = (command_id', (exec_id', exec'));