src/Pure/General/ROOT.ML
author berghofe
Fri, 16 Apr 2004 18:40:21 +0200
changeset 14594 3ff9cfc5c403
parent 14278 ae499452700a
child 14831 7c37c18a6188
permissions -rw-r--r--
Moved symbol.ML to front of file list (due to quote function).
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5018
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/ROOT.ML
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
     3
9119
wenzelm
parents: 9095
diff changeset
     4
Library of general tools --- prefer this over the 'Standard ML Library'.
5018
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
     5
*)
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
     6
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
     7
use "table.ML";
14594
3ff9cfc5c403 Moved symbol.ML to front of file list (due to quote function).
berghofe
parents: 14278
diff changeset
     8
use "scan.ML";
3ff9cfc5c403 Moved symbol.ML to front of file list (due to quote function).
berghofe
parents: 14278
diff changeset
     9
use "source.ML";
3ff9cfc5c403 Moved symbol.ML to front of file list (due to quote function).
berghofe
parents: 14278
diff changeset
    10
use "symbol.ML";
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents: 6116
diff changeset
    11
use "graph.ML";
9119
wenzelm
parents: 9095
diff changeset
    12
use "heap.ML";
5018
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
    13
use "object.ML";
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
    14
use "seq.ML";
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents: 12420
diff changeset
    15
use "susp.ML";
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents: 12420
diff changeset
    16
use "lazy_seq.ML";
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents: 12420
diff changeset
    17
use "lazy_scan.ML";
5018
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
    18
use "name_space.ML";
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
    19
use "position.ML";
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
    20
use "path.ML";
6638
731b4aec2fd6 added url.ML;
wenzelm
parents: 6634
diff changeset
    21
use "url.ML";
5018
ce8e87fad843 General tools.
wenzelm
parents:
diff changeset
    22
use "file.ML";
6317
128e592f5489 added Buffer;
wenzelm
parents: 6222
diff changeset
    23
use "buffer.ML";
5040
78abd4c4802a added General/history.ML;
wenzelm
parents: 5018
diff changeset
    24
use "history.ML";
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents: 5864
diff changeset
    25
use "pretty.ML";
12420
a2a05c952b4d use "xml.ML";
wenzelm
parents: 9119
diff changeset
    26
use "xml.ML";
5864
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    27
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    28
structure PureGeneral =
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    29
struct
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    30
  structure Symtab = Symtab;
6136
166b3353aad5 structure Graph = Graph;
wenzelm
parents: 6134
diff changeset
    31
  structure Graph = Graph;
5864
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    32
  structure Object = Object;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    33
  structure Seq = Seq;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    34
  structure NameSpace = NameSpace;
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    35
  structure Position = Position;
6634
6f74e7aa5b4d moved scan.ML;
wenzelm
parents: 6317
diff changeset
    36
  structure Scan = Scan;
6644
wenzelm
parents: 6638
diff changeset
    37
  structure Source = Source;
6638
731b4aec2fd6 added url.ML;
wenzelm
parents: 6634
diff changeset
    38
  structure Symbol = Symbol;
5864
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    39
  structure Path = Path;
6638
731b4aec2fd6 added url.ML;
wenzelm
parents: 6634
diff changeset
    40
  structure Url = Url;
5864
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    41
  structure File = File;
6317
128e592f5489 added Buffer;
wenzelm
parents: 6222
diff changeset
    42
  structure Buffer = Buffer;
5864
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    43
  structure History = History;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents: 5864
diff changeset
    44
  structure Pretty = Pretty;
12420
a2a05c952b4d use "xml.ML";
wenzelm
parents: 9119
diff changeset
    45
  structure XML = XML;
5864
30b6a3251813 prefixed op;
wenzelm
parents: 5040
diff changeset
    46
end;