# HG changeset patch
# User wenzelm
# Date 1420832357 -3600
# Node ID 4139db32821e1c7ae39f91b6770df94c7b79a121
# Parent  cb3a4caf206d4bee5cc3877450f103413fe9adde
non-strict print_state: display old proof state on failure, e.g. unfinished command;

diff -r cb3a4caf206d -r 4139db32821e src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Jan 09 20:12:42 2015 +0100
+++ b/src/Pure/PIDE/command.ML	Fri Jan 09 20:39:17 2015 +0100
@@ -354,7 +354,7 @@
   print_function "print_state"
     (fn {keywords, command_name, ...} =>
       if Keyword.is_printed keywords command_name then
-        SOME {delay = NONE, pri = 1, persistent = false, strict = true,
+        SOME {delay = NONE, pri = 1, persistent = false, strict = false,
           print_fn = fn _ => fn st => if Toplevel.is_proof st then Toplevel.print_state st else ()}
       else NONE);