src/Pure/ROOT.ML
changeset 22592 97b5290a8c34
parent 22361 d8d96d0122a7
child 22679 68cd69a388e2
     1.1 --- a/src/Pure/ROOT.ML	Wed Apr 04 00:11:26 2007 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Wed Apr 04 00:13:13 2007 +0200
     1.3 @@ -7,9 +7,6 @@
     1.4  val banner = "Pure Isabelle";
     1.5  val version = "Isabelle repository version";    (*filled in automatically!*)
     1.6  
     1.7 -(*if true then some tools will OMIT some proofs*)
     1.8 -val quick_and_dirty = ref false;
     1.9 -
    1.10  print_depth 10;
    1.11  
    1.12  (*fake hiding of private structures*)
    1.13 @@ -18,6 +15,12 @@
    1.14  (*basic tools*)
    1.15  use "General/basics.ML";
    1.16  use "library.ML";
    1.17 +
    1.18 +(*generic non-sense*)
    1.19 +val quick_and_dirty = ref false;
    1.20 +val print_mode = ref ([]: string list);
    1.21 +fun print_mode_active s = member (op =) (! print_mode) s;
    1.22 +
    1.23  cd "General"; use "ROOT.ML"; cd "..";
    1.24  
    1.25  (*fundamental structures*)