diff -r d5d2093ff224 -r c4891dbd5161 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Wed Jul 03 17:50:47 2013 +0200 +++ b/src/Pure/PIDE/document.ML Wed Jul 03 21:32:58 2013 +0200 @@ -459,9 +459,9 @@ val exec' = Command.memo (fn () => let - val (st, _) = Command.memo_result (snd (snd command_exec)); + val (st_malformed, _) = Command.memo_result (snd (snd command_exec)); val tr = read (); - val ({failed}, (st', malformed')) = Command.eval span tr st; + val ({failed}, (st', malformed')) = Command.eval span tr st_malformed; val print = if failed then [] else Command.print tr st'; in ((st', malformed'), print) end); val command_exec' = (command_id', (exec_id', exec'));