src/Pure/General/ROOT.ML
author wenzelm
Sat, 08 Dec 2001 14:42:22 +0100
changeset 12420 a2a05c952b4d
parent 9119 8ca79837b41b
child 14278 ae499452700a
permissions -rw-r--r--
use "xml.ML";
     1 (*  Title:      Pure/General/ROOT.ML
     2     ID:         $Id$
     3 
     4 Library of general tools --- prefer this over the 'Standard ML Library'.
     5 *)
     6 
     7 use "table.ML";
     8 use "graph.ML";
     9 use "heap.ML";
    10 use "object.ML";
    11 use "seq.ML";
    12 use "name_space.ML";
    13 use "position.ML";
    14 use "scan.ML";
    15 use "source.ML";
    16 use "symbol.ML";
    17 use "path.ML";
    18 use "url.ML";
    19 use "file.ML";
    20 use "buffer.ML";
    21 use "history.ML";
    22 use "pretty.ML";
    23 use "xml.ML";
    24 
    25 structure PureGeneral =
    26 struct
    27   structure Symtab = Symtab;
    28   structure Graph = Graph;
    29   structure Object = Object;
    30   structure Seq = Seq;
    31   structure NameSpace = NameSpace;
    32   structure Position = Position;
    33   structure Scan = Scan;
    34   structure Source = Source;
    35   structure Symbol = Symbol;
    36   structure Path = Path;
    37   structure Url = Url;
    38   structure File = File;
    39   structure Buffer = Buffer;
    40   structure History = History;
    41   structure Pretty = Pretty;
    42   structure XML = XML;
    43 end;