src/Pure/General/ROOT.ML
changeset 16136 1cb99d74eebb
parent 14831 7c37c18a6188
child 16465 eb287ce97230
equal deleted inserted replaced
16135:c66545fe72bf 16136:1cb99d74eebb
     4 Library of general tools --- prefer this over the 'Standard ML Library'.
     4 Library of general tools --- prefer this over the 'Standard ML Library'.
     5 *)
     5 *)
     6 
     6 
     7 use "table.ML";
     7 use "table.ML";
     8 use "output.ML";
     8 use "output.ML";
       
     9 use "graph.ML";
       
    10 use "heap.ML";
     9 use "scan.ML";
    11 use "scan.ML";
    10 use "source.ML";
    12 use "source.ML";
    11 use "symbol.ML";
    13 use "symbol.ML";
    12 use "graph.ML";
    14 use "name_space.ML";
    13 use "heap.ML";
       
    14 use "object.ML";
    15 use "object.ML";
    15 use "seq.ML";
    16 use "seq.ML";
    16 use "susp.ML";
    17 use "susp.ML";
    17 use "lazy_seq.ML";
    18 use "lazy_seq.ML";
    18 use "lazy_scan.ML";
    19 use "lazy_scan.ML";
    19 use "name_space.ML";
       
    20 use "position.ML";
    20 use "position.ML";
    21 use "path.ML";
    21 use "path.ML";
    22 use "url.ML";
    22 use "url.ML";
    23 use "file.ML";
    23 use "file.ML";
    24 use "buffer.ML";
    24 use "buffer.ML";
    25 use "history.ML";
    25 use "history.ML";
    26 use "xml.ML";
    26 use "xml.ML";
    27 
       
    28 structure PureGeneral =
       
    29 struct
       
    30   structure Symtab = Symtab;
       
    31   structure Output = Output;
       
    32   structure Graph = Graph;
       
    33   structure Object = Object;
       
    34   structure Seq = Seq;
       
    35   structure NameSpace = NameSpace;
       
    36   structure Position = Position;
       
    37   structure Scan = Scan;
       
    38   structure Source = Source;
       
    39   structure Symbol = Symbol;
       
    40   structure Path = Path;
       
    41   structure Url = Url;
       
    42   structure File = File;
       
    43   structure Buffer = Buffer;
       
    44   structure History = History;
       
    45   structure XML = XML;
       
    46 end;