moved print_mode to General/output.ML; load General/pretty.ML early;
authorwenzelm
Sat May 29 15:00:25 2004 +0200 (2004-05-29)
changeset 14823ebb8499d0fd2
parent 14822 c5fcde6324a2
child 14824 336ade035a34
moved print_mode to General/output.ML; load General/pretty.ML early;
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ROOT.ML	Sat May 29 15:00:14 2004 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Sat May 29 15:00:25 2004 +0200
     1.3 @@ -12,9 +12,6 @@
     1.4  
     1.5  print_depth 10;
     1.6  
     1.7 -(*global flags*)
     1.8 -val print_mode = ref ([]: string list);
     1.9 -
    1.10  (*fake hiding of private structures*)
    1.11  structure Hidden = struct end;
    1.12  
    1.13 @@ -24,6 +21,7 @@
    1.14  
    1.15  (*fundamental structures*)
    1.16  use "term.ML";
    1.17 +use "General/pretty.ML";
    1.18  use "sorts.ML";
    1.19  use "type.ML";
    1.20