clarified bootstrap environment;
authorwenzelm
Tue Apr 05 19:41:58 2016 +0200 (2016-04-05)
changeset 628755a0c06491974
parent 62874 b0194643e64c
child 62876 507c90523113
clarified bootstrap environment;
NEWS
etc/options
src/Pure/ML/ml_env.ML
src/Pure/ML/ml_name_space.ML
src/Pure/ML/ml_pervasive_final.ML
src/Pure/System/options.ML
     1.1 --- a/NEWS	Tue Apr 05 18:25:42 2016 +0200
     1.2 +++ b/NEWS	Tue Apr 05 19:41:58 2016 +0200
     1.3 @@ -235,7 +235,7 @@
     1.4  requiring separate files.
     1.5  
     1.6  * Low-level ML system structures (like PolyML and RunCall) are no longer
     1.7 -exposed to Isabelle/ML user-space. The system option ML_system_unsafe
     1.8 +exposed to Isabelle/ML user-space. The system option ML_system_bootstrap
     1.9  allows to override this for special test situations.
    1.10  
    1.11  * Antiquotation @{make_string} is available during Pure bootstrap --
     2.1 --- a/etc/options	Tue Apr 05 18:25:42 2016 +0200
     2.2 +++ b/etc/options	Tue Apr 05 19:41:58 2016 +0200
     2.3 @@ -126,8 +126,8 @@
     2.4  public option ML_system_64 : bool = false
     2.5    -- "ML system for 64bit platform is used if possible (change requires restart)"
     2.6  
     2.7 -option ML_system_unsafe : bool = false
     2.8 -  -- "provide access to low-level ML system structures"
     2.9 +option ML_system_bootstrap : bool = false
    2.10 +  -- "provide access to low-level ML system structures (unsafe!)"
    2.11  
    2.12  
    2.13  section "Editor Reactivity"
     3.1 --- a/src/Pure/ML/ml_env.ML	Tue Apr 05 18:25:42 2016 +0200
     3.2 +++ b/src/Pure/ML/ml_env.ML	Tue Apr 05 19:41:58 2016 +0200
     3.3 @@ -101,11 +101,11 @@
     3.4              let
     3.5                val val2 =
     3.6                  fold (fn (x, y) =>
     3.7 -                  member (op =) ML_Name_Space.excluded_values x ? Symtab.update (x, y))
     3.8 +                  member (op =) ML_Name_Space.bootstrap_values x ? Symtab.update (x, y))
     3.9                  (#allVal ML_Name_Space.global ()) val1;
    3.10                val structure2 =
    3.11                  fold (fn (x, y) =>
    3.12 -                  member (op =) ML_Name_Space.excluded_structures x ? Symtab.update (x, y))
    3.13 +                  member (op =) ML_Name_Space.bootstrap_structures x ? Symtab.update (x, y))
    3.14                  (#allStruct ML_Name_Space.global ()) structure1;
    3.15              in (val2, type1, fixity1, structure2, signature1, functor1) end);
    3.16      in make_data (bootstrap, tables, sml_tables', breakpoints) end);
     4.1 --- a/src/Pure/ML/ml_name_space.ML	Tue Apr 05 18:25:42 2016 +0200
     4.2 +++ b/src/Pure/ML/ml_name_space.ML	Tue Apr 05 19:41:58 2016 +0200
     4.3 @@ -58,17 +58,22 @@
     4.4    fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
     4.5  
     4.6  
     4.7 -  (* Standard ML name space *)
     4.8 +  (* bootstrap environment *)
     4.9  
    4.10 -  val excluded_values = ["use", "exit"];
    4.11 -  val excluded_structures = ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
    4.12 +  val bootstrap_values =
    4.13 +    ["use", "exit", "ML_system_pretty", "ML_system_pp", "ML_system_overload"];
    4.14 +  val bootstrap_structures =
    4.15 +    ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
    4.16 +
    4.17 +
    4.18 +  (* Standard ML environment *)
    4.19  
    4.20    val sml_val =
    4.21 -    List.filter (fn (a, _) => List.all (fn b => a <> b) excluded_values) (#allVal global ());
    4.22 +    List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_values) (#allVal global ());
    4.23    val sml_type = #allType global ();
    4.24    val sml_fixity = #allFix global ();
    4.25    val sml_structure =
    4.26 -    List.filter (fn (a, _) => List.all (fn b => a <> b) excluded_structures) (#allStruct global ());
    4.27 +    List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_structures) (#allStruct global ());
    4.28    val sml_signature = #allSig global ();
    4.29    val sml_functor = #allFunct global ();
    4.30  end;
     5.1 --- a/src/Pure/ML/ml_pervasive_final.ML	Tue Apr 05 18:25:42 2016 +0200
     5.2 +++ b/src/Pure/ML/ml_pervasive_final.ML	Tue Apr 05 19:41:58 2016 +0200
     5.3 @@ -4,10 +4,11 @@
     5.4  Pervasive ML environment: final setup.
     5.5  *)
     5.6  
     5.7 -if Options.default_bool "ML_system_unsafe" then ()
     5.8 +if Options.default_bool "ML_system_bootstrap" then ()
     5.9  else
    5.10 - (List.app ML_Name_Space.forget_structure (remove (op =) "PolyML" ML_Name_Space.excluded_structures);
    5.11 -  ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
    5.12 +  (List.app ML_Name_Space.forget_structure
    5.13 +    (remove (op =) "PolyML" ML_Name_Space.bootstrap_structures);
    5.14 +   ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
    5.15  
    5.16  structure Output: OUTPUT = Output;  (*seal system channels!*)
    5.17  
     6.1 --- a/src/Pure/System/options.ML	Tue Apr 05 18:25:42 2016 +0200
     6.2 +++ b/src/Pure/System/options.ML	Tue Apr 05 19:41:58 2016 +0200
     6.3 @@ -215,7 +215,9 @@
     6.4    | name =>
     6.5        let val path = Path.explode name in
     6.6          (case try File.read path of
     6.7 -          SOME s => (set_default (decode (YXML.parse_body s)); ignore (try File.rm path))
     6.8 +          SOME s =>
     6.9 +            (set_default (decode (YXML.parse_body s));
    6.10 +             if default_bool "ML_system_bootstrap" then () else ignore (try File.rm path))
    6.11          | NONE => ())
    6.12        end);
    6.13