use setmp_noncritical for sequential Pure bootstrap;
authorwenzelm
Sun, 05 Sep 2010 23:26:16 +0200
changeset 39138 53886463f559
parent 39137 ccb53edd59f0
child 39139 8235606e2b23
use setmp_noncritical for sequential Pure bootstrap;
src/Pure/ProofGeneral/preferences.ML
src/Tools/auto_solve.ML
src/Tools/quickcheck.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Sun Sep 05 23:16:21 2010 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Sun Sep 05 23:26:16 2010 +0200
@@ -78,7 +78,7 @@
 
 (* preferences of Pure *)
 
-val proof_pref = setmp_CRITICAL Proofterm.proofs 1 (fn () =>
+val proof_pref = setmp_noncritical Proofterm.proofs 1 (fn () =>
   let
     fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2);
     fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
@@ -167,7 +167,7 @@
   thm_deps_pref];
 
 val proof_preferences =
- [setmp_CRITICAL quick_and_dirty true (fn () =>
+ [setmp_noncritical quick_and_dirty true (fn () =>
     bool_pref quick_and_dirty
       "quick-and-dirty"
       "Take a few short cuts") (),
--- a/src/Tools/auto_solve.ML	Sun Sep 05 23:16:21 2010 +0200
+++ b/src/Tools/auto_solve.ML	Sun Sep 05 23:26:16 2010 +0200
@@ -33,7 +33,7 @@
 
 val _ =
   ProofGeneralPgip.add_preference Preferences.category_tracing
-  (setmp_CRITICAL auto true (fn () =>
+  (setmp_noncritical auto true (fn () =>
     Preferences.bool_pref auto
       "auto-solve"
       "Try to solve newly declared lemmas with existing theorems.") ());
--- a/src/Tools/quickcheck.ML	Sun Sep 05 23:16:21 2010 +0200
+++ b/src/Tools/quickcheck.ML	Sun Sep 05 23:26:16 2010 +0200
@@ -40,7 +40,7 @@
 
 val _ =
   ProofGeneralPgip.add_preference Preferences.category_tracing
-  (setmp_CRITICAL auto true (fn () =>
+  (setmp_noncritical auto true (fn () =>
     Preferences.bool_pref auto
       "auto-quickcheck"
       "Whether to run Quickcheck automatically.") ());