# HG changeset patch
# User wenzelm
# Date 1378303425 -7200
# Node ID d598b6231ff788e0caf44ddd149ed338922b11fa
# Parent  c09f4005d6bd446aafedf3dc4d1686e6e8b22abf
non-persistent print_state: trade-off between JVM space vs. ML time;

diff -r c09f4005d6bd -r d598b6231ff7 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed Sep 04 15:27:24 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Wed Sep 04 16:03:45 2013 +0200
@@ -294,7 +294,7 @@
 val _ =
   print_function "print_state"
     (fn {command_name, ...} =>
-      SOME {delay = NONE, pri = 1, persistent = true, strict = true,
+      SOME {delay = NONE, pri = 1, persistent = false, strict = true,
         print_fn = fn tr => fn st' =>
           let
             val is_init = Keyword.is_theory_begin command_name;