author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 24633  0a3a02066244 
child 25715  3d1d281b2471 
permissions  rwrr 
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 