simplified bootstrap: critical structures remain accessible in ML_Root context;
authorwenzelm
Wed Apr 06 11:57:21 2016 +0200 (2016-04-06)
changeset 6288672c475e03e22
parent 62885 108630498c00
child 62887 6b2c60ebd915
simplified bootstrap: critical structures remain accessible in ML_Root context;
NEWS
etc/options
src/Pure/ML/ml_compiler0.ML
src/Pure/ML/ml_pervasive1.ML
src/Pure/ROOT1.ML
     1.1 --- a/NEWS	Wed Apr 06 11:50:07 2016 +0200
     1.2 +++ b/NEWS	Wed Apr 06 11:57:21 2016 +0200
     1.3 @@ -235,8 +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_bootstrap
     1.8 -allows to override this for special test situations.
     1.9 +exposed to Isabelle/ML user-space. Potential INCOMPATIBILITY.
    1.10  
    1.11  * Antiquotation @{make_string} is available during Pure bootstrap --
    1.12  with approximative output quality.
     2.1 --- a/etc/options	Wed Apr 06 11:50:07 2016 +0200
     2.2 +++ b/etc/options	Wed Apr 06 11:57:21 2016 +0200
     2.3 @@ -126,9 +126,6 @@
     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_bootstrap : bool = false
     2.8 -  -- "provide access to low-level ML system structures (unsafe!)"
     2.9 -
    2.10  
    2.11  section "Editor Reactivity"
    2.12  
     3.1 --- a/src/Pure/ML/ml_compiler0.ML	Wed Apr 06 11:50:07 2016 +0200
     3.2 +++ b/src/Pure/ML/ml_compiler0.ML	Wed Apr 06 11:57:21 2016 +0200
     3.3 @@ -154,4 +154,4 @@
     3.4         ("addPrettyPrinter", "ML_system_pp"),
     3.5         ("addOverload", "ML_system_overload")]))
     3.6    {debug = false, file = "", line = 0, verbose = false}
     3.7 -  "open PolyML RunCall";
     3.8 +  "open PolyML RunCall" handle ERROR _ => ();
     4.1 --- a/src/Pure/ML/ml_pervasive1.ML	Wed Apr 06 11:50:07 2016 +0200
     4.2 +++ b/src/Pure/ML/ml_pervasive1.ML	Wed Apr 06 11:57:21 2016 +0200
     4.3 @@ -4,11 +4,10 @@
     4.4  Pervasive ML environment: final setup.
     4.5  *)
     4.6  
     4.7 -if Options.default_bool "ML_system_bootstrap" then ()
     4.8 -else
     4.9 -  (List.app ML_Name_Space.forget_structure
    4.10 -    (remove (op =) "PolyML" ML_Name_Space.bootstrap_structures);
    4.11 -   ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
    4.12 +List.app ML_Name_Space.forget_structure
    4.13 +  (remove (op =) "PolyML" ML_Name_Space.bootstrap_structures);
    4.14 +
    4.15 +structure PolyML = struct structure IntInf = PolyML.IntInf end;
    4.16  
    4.17  Proofterm.proofs := 0;
    4.18  
     5.1 --- a/src/Pure/ROOT1.ML	Wed Apr 06 11:50:07 2016 +0200
     5.2 +++ b/src/Pure/ROOT1.ML	Wed Apr 06 11:57:21 2016 +0200
     5.3 @@ -1,6 +1,6 @@
     5.4  (*** Isabelle/Pure bootstrap: final setup ***)
     5.5  
     5.6  use_thy "Pure";
     5.7 +use_thy "ML_Root";
     5.8  
     5.9  use "ML/ml_pervasive1.ML";
    5.10 -use_thy "ML_Root";