early setup of secure operations (again, cf. deddd77112b7) -- NB: fix_ints is required for bootstrap;
authorwenzelm
Tue Jun 02 13:15:16 2009 +0200 (2009-06-02)
changeset 31335ba5b7749fa61
parent 31334 999fa9e1dbdd
child 31365 7f65653e3d48
early setup of secure operations (again, cf. deddd77112b7) -- NB: fix_ints is required for bootstrap;
late setup of ML_Env and ML_Compiler;
src/Pure/General/ROOT.ML
src/Pure/Isar/ROOT.ML
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/General/ROOT.ML	Mon Jun 01 23:28:07 2009 +0200
     1.2 +++ b/src/Pure/General/ROOT.ML	Tue Jun 02 13:15:16 2009 +0200
     1.3 @@ -16,6 +16,10 @@
     1.4  use "position.ML";
     1.5  use "symbol_pos.ML";
     1.6  use "antiquote.ML";
     1.7 +use "../ML/ml_lex.ML";
     1.8 +use "../ML/ml_parse.ML";
     1.9 +use "secure.ML";
    1.10 +
    1.11  use "integer.ML";
    1.12  use "stack.ML";
    1.13  use "queue.ML";
    1.14 @@ -30,6 +34,7 @@
    1.15  use "path.ML";
    1.16  use "url.ML";
    1.17  use "buffer.ML";
    1.18 +use "file.ML";
    1.19  use "xml.ML";
    1.20  use "yxml.ML";
    1.21  
     2.1 --- a/src/Pure/Isar/ROOT.ML	Mon Jun 01 23:28:07 2009 +0200
     2.2 +++ b/src/Pure/Isar/ROOT.ML	Tue Jun 02 13:15:16 2009 +0200
     2.3 @@ -24,6 +24,13 @@
     2.4  use "outer_parse.ML";
     2.5  use "value_parse.ML";
     2.6  use "args.ML";
     2.7 +
     2.8 +(*ML support*)
     2.9 +use "../ML/ml_syntax.ML";
    2.10 +use "../ML/ml_env.ML";
    2.11 +if ml_system = "polyml-experimental"
    2.12 +then use "../ML/ml_compiler_polyml-5.3.ML"
    2.13 +else use "../ML/ml_compiler.ML";
    2.14  use "../ML/ml_context.ML";
    2.15  
    2.16  (*theory sources*)
     3.1 --- a/src/Pure/ROOT.ML	Mon Jun 01 23:28:07 2009 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Tue Jun 02 13:15:16 2009 +0200
     3.3 @@ -47,19 +47,6 @@
     3.4  
     3.5  use "type_infer.ML";
     3.6  
     3.7 -(*ML support*)
     3.8 -use "ML/ml_lex.ML";
     3.9 -use "ML/ml_parse.ML";
    3.10 -use "ML/ml_syntax.ML";
    3.11 -use "ML/ml_env.ML";
    3.12 -
    3.13 -use "General/secure.ML";
    3.14 -use "General/file.ML";
    3.15 -
    3.16 -if ml_system = "polyml-experimental"
    3.17 -then use "ML/ml_compiler_polyml-5.3.ML"
    3.18 -else use "ML/ml_compiler.ML";
    3.19 -
    3.20  (*core of tactical proof system*)
    3.21  use "net.ML";
    3.22  use "item_net.ML";