non-persistent print_state: trade-off between JVM space vs. ML time;
authorwenzelm
Wed Sep 04 16:03:45 2013 +0200 (2013-09-04 ago)
changeset 53404d598b6231ff7
parent 53403 c09f4005d6bd
child 53405 ed2b48af04d9
non-persistent print_state: trade-off between JVM space vs. ML time;
src/Pure/PIDE/command.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Wed Sep 04 15:27:24 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Wed Sep 04 16:03:45 2013 +0200
     1.3 @@ -294,7 +294,7 @@
     1.4  val _ =
     1.5    print_function "print_state"
     1.6      (fn {command_name, ...} =>
     1.7 -      SOME {delay = NONE, pri = 1, persistent = true, strict = true,
     1.8 +      SOME {delay = NONE, pri = 1, persistent = false, strict = true,
     1.9          print_fn = fn tr => fn st' =>
    1.10            let
    1.11              val is_init = Keyword.is_theory_begin command_name;