tuned;

--- 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'));