author | wenzelm |
Sat, 08 Dec 2001 14:42:22 +0100 | |
changeset 12420 | a2a05c952b4d |
parent 9119 | 8ca79837b41b |
child 14278 | ae499452700a |
permissions | -rw-r--r-- |
1 (* Title: Pure/General/ROOT.ML
2 ID: $Id$
4 Library of general tools --- prefer this over the 'Standard ML Library'.
5 *)
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";
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;