src/Pure/General/ROOT.ML
author skalberg
Fri, 05 Dec 2003 19:39:39 +0100
changeset 14278 ae499452700a
parent 12420 a2a05c952b4d
child 14594 3ff9cfc5c403
permissions -rw-r--r--
Added lazy sequences and parser combinators for same.
wenzelm@5018
     1
(*  Title:      Pure/General/ROOT.ML
wenzelm@5018
     2
    ID:         $Id$
wenzelm@5018
     3
wenzelm@9119
     4
Library of general tools --- prefer this over the 'Standard ML Library'.
wenzelm@5018
     5
*)
wenzelm@5018
     6
wenzelm@5018
     7
use "table.ML";
wenzelm@6134
     8
use "graph.ML";
wenzelm@9119
     9
use "heap.ML";
wenzelm@5018
    10
use "object.ML";
wenzelm@5018
    11
use "seq.ML";
skalberg@14278
    12
use "susp.ML";
skalberg@14278
    13
use "lazy_seq.ML";
skalberg@14278
    14
use "lazy_scan.ML";
wenzelm@5018
    15
use "name_space.ML";
wenzelm@5018
    16
use "position.ML";
wenzelm@6634
    17
use "scan.ML";
wenzelm@6638
    18
use "source.ML";
wenzelm@6638
    19
use "symbol.ML";
wenzelm@5018
    20
use "path.ML";
wenzelm@6638
    21
use "url.ML";
wenzelm@5018
    22
use "file.ML";
wenzelm@6317
    23
use "buffer.ML";
wenzelm@5040
    24
use "history.ML";
wenzelm@6116
    25
use "pretty.ML";
wenzelm@12420
    26
use "xml.ML";
wenzelm@5864
    27
wenzelm@5864
    28
structure PureGeneral =
wenzelm@5864
    29
struct
wenzelm@5864
    30
  structure Symtab = Symtab;
wenzelm@6136
    31
  structure Graph = Graph;
wenzelm@5864
    32
  structure Object = Object;
wenzelm@5864
    33
  structure Seq = Seq;
wenzelm@5864
    34
  structure NameSpace = NameSpace;
wenzelm@5864
    35
  structure Position = Position;
wenzelm@6634
    36
  structure Scan = Scan;
wenzelm@6644
    37
  structure Source = Source;
wenzelm@6638
    38
  structure Symbol = Symbol;
wenzelm@5864
    39
  structure Path = Path;
wenzelm@6638
    40
  structure Url = Url;
wenzelm@5864
    41
  structure File = File;
wenzelm@6317
    42
  structure Buffer = Buffer;
wenzelm@5864
    43
  structure History = History;
wenzelm@6116
    44
  structure Pretty = Pretty;
wenzelm@12420
    45
  structure XML = XML;
wenzelm@5864
    46
end;