# HG changeset patch
# User wenzelm
# Date 1175638393 -7200
# Node ID 97b5290a8c348470be9b6d4a3b941973e63c26c3
# Parent  7d1015d59f24390f3f8ff3579b6fea36fbac7f67
added print_mode (generic non-sense);

diff -r 7d1015d59f24 -r 97b5290a8c34 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*)