moved print_mode to ROOT.ML
authoroheimb
Fri Jan 29 17:10:26 1999 +0100 (1999-01-29)
changeset 6164a0e9501d56f8
parent 6163 be8234f37e48
child 6165 a7d74bf9da52
moved print_mode to ROOT.ML
src/Pure/ROOT.ML
src/Pure/Syntax/printer.ML
     1.1 --- a/src/Pure/ROOT.ML	Fri Jan 29 17:08:20 1999 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Fri Jan 29 17:10:26 1999 +0100
     1.3 @@ -11,6 +11,11 @@
     1.4  
     1.5  print_depth 1;
     1.6  
     1.7 +(* global flags *)
     1.8 +val print_mode = ref ([]:string list);
     1.9 +(*if true then some packages will OMIT SOME PROOFS*)
    1.10 +val quick_and_dirty = ref false;
    1.11 +
    1.12  (*fake hiding of private structures*)
    1.13  structure Hidden = struct end;
    1.14  
    1.15 @@ -63,9 +68,6 @@
    1.16  
    1.17  use "install_pp.ML";
    1.18  
    1.19 -(*if true then some packages will OMIT SOME PROOFS*)
    1.20 -val quick_and_dirty = ref false;
    1.21 -
    1.22  (*several object-logics declare theories that hide basis library structures*)
    1.23  structure BasisLibrary =
    1.24  struct
     2.1 --- a/src/Pure/Syntax/printer.ML	Fri Jan 29 17:08:20 1999 +0100
     2.2 +++ b/src/Pure/Syntax/printer.ML	Fri Jan 29 17:10:26 1999 +0100
     2.3 @@ -11,7 +11,6 @@
     2.4    val show_sorts: bool ref
     2.5    val show_types: bool ref
     2.6    val show_no_free_types: bool ref
     2.7 -  val print_mode: string list ref
     2.8  end;
     2.9  
    2.10  signature PRINTER =
    2.11 @@ -42,7 +41,6 @@
    2.12  val show_sorts = ref false;
    2.13  val show_brackets = ref false;
    2.14  val show_no_free_types = ref false;
    2.15 -val print_mode = ref ([]:string list);
    2.16  
    2.17  
    2.18