added print_mode (generic non-sense);
authorwenzelm
Wed, 04 Apr 2007 00:13:13 +0200
changeset 22592 97b5290a8c34
parent 22591 7d1015d59f24
child 22593 de39593f2948
added print_mode (generic non-sense);
src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Apr 04 00:11:26 2007 +0200
+++ b/src/Pure/ROOT.ML	Wed Apr 04 00:13:13 2007 +0200
@@ -7,9 +7,6 @@
 val banner = "Pure Isabelle";
 val version = "Isabelle repository version";    (*filled in automatically!*)
 
-(*if true then some tools will OMIT some proofs*)
-val quick_and_dirty = ref false;
-
 print_depth 10;
 
 (*fake hiding of private structures*)
@@ -18,6 +15,12 @@
 (*basic tools*)
 use "General/basics.ML";
 use "library.ML";
+
+(*generic non-sense*)
+val quick_and_dirty = ref false;
+val print_mode = ref ([]: string list);
+fun print_mode_active s = member (op =) (! print_mode) s;
+
 cd "General"; use "ROOT.ML"; cd "..";
 
 (*fundamental structures*)