author | huffman |
Thu, 26 May 2005 02:23:27 +0200 | |
changeset 16081 | 81a4b4a245b0 |
parent 14831 | 7c37c18a6188 |
child 16136 | 1cb99d74eebb |
permissions | -rw-r--r-- |
5018 | 1 |
(* Title: Pure/General/ROOT.ML |
2 |
ID: $Id$ |
|
3 |
||
9119 | 4 |
Library of general tools --- prefer this over the 'Standard ML Library'. |
5018 | 5 |
*) |
6 |
||
7 |
use "table.ML"; |
|
14831
7c37c18a6188
added Pure/General/output.ML; load Pure/General/pretty.ML early in Pure/ROOT.ML;
wenzelm
parents:
14594
diff
changeset
|
8 |
use "output.ML"; |
14594
3ff9cfc5c403
Moved symbol.ML to front of file list (due to quote function).
berghofe
parents:
14278
diff
changeset
|
9 |
use "scan.ML"; |
3ff9cfc5c403
Moved symbol.ML to front of file list (due to quote function).
berghofe
parents:
14278
diff
changeset
|
10 |
use "source.ML"; |
3ff9cfc5c403
Moved symbol.ML to front of file list (due to quote function).
berghofe
parents:
14278
diff
changeset
|
11 |
use "symbol.ML"; |
6134 | 12 |
use "graph.ML"; |
9119 | 13 |
use "heap.ML"; |
5018 | 14 |
use "object.ML"; |
15 |
use "seq.ML"; |
|
14278
ae499452700a
Added lazy sequences and parser combinators for same.
skalberg
parents:
12420
diff
changeset
|
16 |
use "susp.ML"; |
ae499452700a
Added lazy sequences and parser combinators for same.
skalberg
parents:
12420
diff
changeset
|
17 |
use "lazy_seq.ML"; |
ae499452700a
Added lazy sequences and parser combinators for same.
skalberg
parents:
12420
diff
changeset
|
18 |
use "lazy_scan.ML"; |
5018 | 19 |
use "name_space.ML"; |
20 |
use "position.ML"; |
|
21 |
use "path.ML"; |
|
6638 | 22 |
use "url.ML"; |
5018 | 23 |
use "file.ML"; |
6317 | 24 |
use "buffer.ML"; |
5040 | 25 |
use "history.ML"; |
12420 | 26 |
use "xml.ML"; |
5864 | 27 |
|
28 |
structure PureGeneral = |
|
29 |
struct |
|
30 |
structure Symtab = Symtab; |
|
14831
7c37c18a6188
added Pure/General/output.ML; load Pure/General/pretty.ML early in Pure/ROOT.ML;
wenzelm
parents:
14594
diff
changeset
|
31 |
structure Output = Output; |
6136 | 32 |
structure Graph = Graph; |
5864 | 33 |
structure Object = Object; |
34 |
structure Seq = Seq; |
|
35 |
structure NameSpace = NameSpace; |
|
36 |
structure Position = Position; |
|
6634 | 37 |
structure Scan = Scan; |
6644 | 38 |
structure Source = Source; |
6638 | 39 |
structure Symbol = Symbol; |
5864 | 40 |
structure Path = Path; |
6638 | 41 |
structure Url = Url; |
5864 | 42 |
structure File = File; |
6317 | 43 |
structure Buffer = Buffer; |
5864 | 44 |
structure History = History; |
12420 | 45 |
structure XML = XML; |
5864 | 46 |
end; |