added Pure/General/output.ML; load Pure/General/pretty.ML early in Pure/ROOT.ML;
authorwenzelm
Sat May 29 15:05:37 2004 +0200 (2004-05-29)
changeset 148317c37c18a6188
parent 14830 faa4865ba1ce
child 14832 6589a58f57cb
added Pure/General/output.ML; load Pure/General/pretty.ML early in Pure/ROOT.ML;
src/Pure/General/ROOT.ML
     1.1 --- a/src/Pure/General/ROOT.ML	Sat May 29 15:05:25 2004 +0200
     1.2 +++ b/src/Pure/General/ROOT.ML	Sat May 29 15:05:37 2004 +0200
     1.3 @@ -5,6 +5,7 @@
     1.4  *)
     1.5  
     1.6  use "table.ML";
     1.7 +use "output.ML";
     1.8  use "scan.ML";
     1.9  use "source.ML";
    1.10  use "symbol.ML";
    1.11 @@ -22,12 +23,12 @@
    1.12  use "file.ML";
    1.13  use "buffer.ML";
    1.14  use "history.ML";
    1.15 -use "pretty.ML";
    1.16  use "xml.ML";
    1.17  
    1.18  structure PureGeneral =
    1.19  struct
    1.20    structure Symtab = Symtab;
    1.21 +  structure Output = Output;
    1.22    structure Graph = Graph;
    1.23    structure Object = Object;
    1.24    structure Seq = Seq;
    1.25 @@ -41,6 +42,5 @@
    1.26    structure File = File;
    1.27    structure Buffer = Buffer;
    1.28    structure History = History;
    1.29 -  structure Pretty = Pretty;
    1.30    structure XML = XML;
    1.31  end;