author | wenzelm |
Wed, 13 Jan 1999 12:44:33 +0100 | |
changeset 6116 | 8ba2f25610f7 |
parent 5864 | 30b6a3251813 |
child 6134 | ec6092b0599d |
permissions | -rw-r--r-- |
5018 | 1 |
(* Title: Pure/General/ROOT.ML |
2 |
ID: $Id$ |
|
3 |
||
4 |
General tools. |
|
5 |
*) |
|
6 |
||
7 |
use "table.ML"; |
|
8 |
use "object.ML"; |
|
9 |
use "seq.ML"; |
|
10 |
use "name_space.ML"; |
|
11 |
use "position.ML"; |
|
12 |
use "path.ML"; |
|
13 |
use "file.ML"; |
|
5040 | 14 |
use "history.ML"; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
5864
diff
changeset
|
15 |
use "scan.ML"; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
5864
diff
changeset
|
16 |
use "source.ML"; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
5864
diff
changeset
|
17 |
use "symbol.ML"; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
5864
diff
changeset
|
18 |
use "pretty.ML"; |
5864 | 19 |
|
20 |
structure PureGeneral = |
|
21 |
struct |
|
22 |
structure Symtab = Symtab; |
|
23 |
structure Object = Object; |
|
24 |
structure Seq = Seq; |
|
25 |
structure NameSpace = NameSpace; |
|
26 |
structure Position = Position; |
|
27 |
structure Path = Path; |
|
28 |
structure File = File; |
|
29 |
structure History = History; |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
5864
diff
changeset
|
30 |
structure Scan = Scan; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
5864
diff
changeset
|
31 |
structure Source = Source; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
5864
diff
changeset
|
32 |
structure Symbol = Symbol; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
5864
diff
changeset
|
33 |
structure Pretty = Pretty; |
5864 | 34 |
end; |