clarified modules;
authorwenzelm
Mon Apr 04 20:20:47 2016 +0200 (2016-04-04)
changeset 62852dd5f3a6fee73
parent 62851 07eea2843b82
child 62853 8e54fd480809
clarified modules;
src/Pure/ML/ml_final.ML
src/Pure/ML/ml_pervasive.ML
src/Pure/ML/ml_pervasive_final.ML
src/Pure/ML/ml_pervasive_initial.ML
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ML/ml_final.ML	Mon Apr 04 20:07:08 2016 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,19 +0,0 @@
     1.4 -(*  Title:      Pure/ML/ml_final.ML
     1.5 -    Author:     Makarius
     1.6 -
     1.7 -Final setup of ML environment.
     1.8 -*)
     1.9 -
    1.10 -if Options.default_bool "ML_system_unsafe" then ()
    1.11 -else
    1.12 -  (List.app ML_Name_Space.forget_structure
    1.13 -    ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
    1.14 -   ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
    1.15 -
    1.16 -structure Output: OUTPUT = Output;  (*seal system channels!*)
    1.17 -
    1.18 -structure Pure = struct val thy = Thy_Info.pure_theory () end;
    1.19 -
    1.20 -Proofterm.proofs := 0;
    1.21 -
    1.22 -Context.set_thread_data NONE;
     2.1 --- a/src/Pure/ML/ml_pervasive.ML	Mon Apr 04 20:07:08 2016 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,28 +0,0 @@
     2.4 -(*  Title:      Pure/ML/ml_pervasive.ML
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -Pervasive ML environment.
     2.8 -*)
     2.9 -
    2.10 -structure PolyML_Pretty =
    2.11 -struct
    2.12 -  datatype context = datatype PolyML.context;
    2.13 -  datatype pretty = datatype PolyML.pretty;
    2.14 -end;
    2.15 -
    2.16 -val seconds = Time.fromReal;
    2.17 -
    2.18 -val _ =
    2.19 -  List.app ML_Name_Space.forget_val
    2.20 -    ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
    2.21 -
    2.22 -val ord = SML90.ord;
    2.23 -val chr = SML90.chr;
    2.24 -val raw_explode = SML90.explode;
    2.25 -val implode = SML90.implode;
    2.26 -
    2.27 -val pointer_eq = PolyML.pointerEq;
    2.28 -
    2.29 -val error_depth = PolyML.error_depth;
    2.30 -
    2.31 -open Thread;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/ML/ml_pervasive_final.ML	Mon Apr 04 20:20:47 2016 +0200
     3.3 @@ -0,0 +1,19 @@
     3.4 +(*  Title:      Pure/ML/ml_pervasive_final.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Pervasive ML environment: final setup.
     3.8 +*)
     3.9 +
    3.10 +if Options.default_bool "ML_system_unsafe" then ()
    3.11 +else
    3.12 +  (List.app ML_Name_Space.forget_structure
    3.13 +    ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
    3.14 +   ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
    3.15 +
    3.16 +structure Output: OUTPUT = Output;  (*seal system channels!*)
    3.17 +
    3.18 +structure Pure = struct val thy = Thy_Info.pure_theory () end;
    3.19 +
    3.20 +Proofterm.proofs := 0;
    3.21 +
    3.22 +Context.set_thread_data NONE;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/ML/ml_pervasive_initial.ML	Mon Apr 04 20:20:47 2016 +0200
     4.3 @@ -0,0 +1,28 @@
     4.4 +(*  Title:      Pure/ML/ml_pervasive_initial.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Pervasive ML environment: initial setup.
     4.8 +*)
     4.9 +
    4.10 +structure PolyML_Pretty =
    4.11 +struct
    4.12 +  datatype context = datatype PolyML.context;
    4.13 +  datatype pretty = datatype PolyML.pretty;
    4.14 +end;
    4.15 +
    4.16 +val seconds = Time.fromReal;
    4.17 +
    4.18 +val _ =
    4.19 +  List.app ML_Name_Space.forget_val
    4.20 +    ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
    4.21 +
    4.22 +val ord = SML90.ord;
    4.23 +val chr = SML90.chr;
    4.24 +val raw_explode = SML90.explode;
    4.25 +val implode = SML90.implode;
    4.26 +
    4.27 +val pointer_eq = PolyML.pointerEq;
    4.28 +
    4.29 +val error_depth = PolyML.error_depth;
    4.30 +
    4.31 +open Thread;
     5.1 --- a/src/Pure/ROOT	Mon Apr 04 20:07:08 2016 +0200
     5.2 +++ b/src/Pure/ROOT	Mon Apr 04 20:20:47 2016 +0200
     5.3 @@ -108,12 +108,12 @@
     5.4      "ML/ml_context.ML"
     5.5      "ML/ml_debugger.ML"
     5.6      "ML/ml_env.ML"
     5.7 -    "ML/ml_final.ML"
     5.8      "ML/ml_heap.ML"
     5.9      "ML/ml_lex.ML"
    5.10      "ML/ml_name_space.ML"
    5.11      "ML/ml_options.ML"
    5.12 -    "ML/ml_pervasive.ML"
    5.13 +    "ML/ml_pervasive_final.ML"
    5.14 +    "ML/ml_pervasive_initial.ML"
    5.15      "ML/ml_pp.ML"
    5.16      "ML/ml_pretty.ML"
    5.17      "ML/ml_profiling.ML"
     6.1 --- a/src/Pure/ROOT.ML	Mon Apr 04 20:07:08 2016 +0200
     6.2 +++ b/src/Pure/ROOT.ML	Mon Apr 04 20:20:47 2016 +0200
     6.3 @@ -6,7 +6,7 @@
     6.4  
     6.5  use "ML/ml_system.ML";
     6.6  use "ML/ml_name_space.ML";
     6.7 -use "ML/ml_pervasive.ML";
     6.8 +use "ML/ml_pervasive_initial.ML";
     6.9  
    6.10  if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
    6.11  else use "ML/fixed_int_dummy.ML";
    6.12 @@ -338,7 +338,4 @@
    6.13  
    6.14  use_thy "Pure";
    6.15  
    6.16 -
    6.17 -(* final ML setup *)
    6.18 -
    6.19 -use "ML/ml_final.ML";
    6.20 +use "ML/ml_pervasive_final.ML";