| author | wenzelm | 
| Thu, 03 Jan 2008 17:50:42 +0100 | |
| changeset 25808 | c7aaa3f6f0ac | 
| parent 25728 | 71e33d95ac55 | 
| child 26077 | 1498f0362362 | 
| permissions | -rw-r--r-- | 
| 5018 | 1  | 
(* Title: Pure/General/ROOT.ML  | 
2  | 
ID: $Id$  | 
|
3  | 
||
| 18132 | 4  | 
Library of general tools.  | 
| 5018 | 5  | 
*)  | 
6  | 
||
| 23823 | 7  | 
use "print_mode.ML";  | 
| 17152 | 8  | 
use "alist.ML";  | 
| 5018 | 9  | 
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
 | 
10  | 
use "output.ML";  | 
| 23636 | 11  | 
use "markup.ML";  | 
| 
14594
 
3ff9cfc5c403
Moved symbol.ML to front of file list (due to quote function).
 
berghofe 
parents: 
14278 
diff
changeset
 | 
12  | 
use "scan.ML";  | 
| 
 
3ff9cfc5c403
Moved symbol.ML to front of file list (due to quote function).
 
berghofe 
parents: 
14278 
diff
changeset
 | 
13  | 
use "source.ML";  | 
| 
 
3ff9cfc5c403
Moved symbol.ML to front of file list (due to quote function).
 
berghofe 
parents: 
14278 
diff
changeset
 | 
14  | 
use "symbol.ML";  | 
| 24578 | 15  | 
use "../ML/ml_lex.ML";  | 
| 24602 | 16  | 
use "../ML/ml_parse.ML";  | 
| 
21769
 
b82f344f7922
load secure.ML after symbol.ML, when default output is active;
 
wenzelm 
parents: 
21157 
diff
changeset
 | 
17  | 
use "secure.ML";  | 
| 
24445
 
cad0644294a9
tuned load order -- minimizes modules before Secure;
 
wenzelm 
parents: 
24264 
diff
changeset
 | 
18  | 
|
| 
24633
 
0a3a02066244
moved Tools/integer.ML to Pure/General/integer.ML;
 
wenzelm 
parents: 
24602 
diff
changeset
 | 
19  | 
use "integer.ML";  | 
| 
24445
 
cad0644294a9
tuned load order -- minimizes modules before Secure;
 
wenzelm 
parents: 
24264 
diff
changeset
 | 
20  | 
use "stack.ML";  | 
| 
 
cad0644294a9
tuned load order -- minimizes modules before Secure;
 
wenzelm 
parents: 
24264 
diff
changeset
 | 
21  | 
use "heap.ML";  | 
| 
 
cad0644294a9
tuned load order -- minimizes modules before Secure;
 
wenzelm 
parents: 
24264 
diff
changeset
 | 
22  | 
use "ord_list.ML";  | 
| 
 
cad0644294a9
tuned load order -- minimizes modules before Secure;
 
wenzelm 
parents: 
24264 
diff
changeset
 | 
23  | 
use "balanced_tree.ML";  | 
| 
 
cad0644294a9
tuned load order -- minimizes modules before Secure;
 
wenzelm 
parents: 
24264 
diff
changeset
 | 
24  | 
use "graph.ML";  | 
| 16136 | 25  | 
use "name_space.ML";  | 
| 5018 | 26  | 
use "seq.ML";  | 
| 20594 | 27  | 
use "susp.ML";  | 
| 5018 | 28  | 
use "path.ML";  | 
| 23696 | 29  | 
use "position.ML";  | 
| 6638 | 30  | 
use "url.ML";  | 
| 5018 | 31  | 
use "file.ML";  | 
| 6317 | 32  | 
use "buffer.ML";  | 
| 5040 | 33  | 
use "history.ML";  | 
| 24264 | 34  | 
use "xml.ML";  | 
35  |