moved print_mode to ROOT.ML
authoroheimb
Fri, 29 Jan 1999 17:10:26 +0100
changeset 6164 a0e9501d56f8
parent 6163 be8234f37e48
child 6165 a7d74bf9da52
moved print_mode to ROOT.ML
src/Pure/ROOT.ML
src/Pure/Syntax/printer.ML
--- a/src/Pure/ROOT.ML	Fri Jan 29 17:08:20 1999 +0100
+++ b/src/Pure/ROOT.ML	Fri Jan 29 17:10:26 1999 +0100
@@ -11,6 +11,11 @@
 
 print_depth 1;
 
+(* global flags *)
+val print_mode = ref ([]:string list);
+(*if true then some packages will OMIT SOME PROOFS*)
+val quick_and_dirty = ref false;
+
 (*fake hiding of private structures*)
 structure Hidden = struct end;
 
@@ -63,9 +68,6 @@
 
 use "install_pp.ML";
 
-(*if true then some packages will OMIT SOME PROOFS*)
-val quick_and_dirty = ref false;
-
 (*several object-logics declare theories that hide basis library structures*)
 structure BasisLibrary =
 struct
--- a/src/Pure/Syntax/printer.ML	Fri Jan 29 17:08:20 1999 +0100
+++ b/src/Pure/Syntax/printer.ML	Fri Jan 29 17:10:26 1999 +0100
@@ -11,7 +11,6 @@
   val show_sorts: bool ref
   val show_types: bool ref
   val show_no_free_types: bool ref
-  val print_mode: string list ref
 end;
 
 signature PRINTER =
@@ -42,7 +41,6 @@
 val show_sorts = ref false;
 val show_brackets = ref false;
 val show_no_free_types = ref false;
-val print_mode = ref ([]:string list);