# HG changeset patch
# User wenzelm
# Date 1459936641 -7200
# Node ID 72c475e03e226d0ea240249f49a16f0bd86d3e61
# Parent  108630498c0055243345de758034111b493c45f1
simplified bootstrap: critical structures remain accessible in ML_Root context;

diff -r 108630498c00 -r 72c475e03e22 NEWS
--- a/NEWS	Wed Apr 06 11:50:07 2016 +0200
+++ b/NEWS	Wed Apr 06 11:57:21 2016 +0200
@@ -235,8 +235,7 @@
 requiring separate files.
 
 * Low-level ML system structures (like PolyML and RunCall) are no longer
-exposed to Isabelle/ML user-space. The system option ML_system_bootstrap
-allows to override this for special test situations.
+exposed to Isabelle/ML user-space. Potential INCOMPATIBILITY.
 
 * Antiquotation @{make_string} is available during Pure bootstrap --
 with approximative output quality.
diff -r 108630498c00 -r 72c475e03e22 etc/options
--- a/etc/options	Wed Apr 06 11:50:07 2016 +0200
+++ b/etc/options	Wed Apr 06 11:57:21 2016 +0200
@@ -126,9 +126,6 @@
 public option ML_system_64 : bool = false
   -- "ML system for 64bit platform is used if possible (change requires restart)"
 
-option ML_system_bootstrap : bool = false
-  -- "provide access to low-level ML system structures (unsafe!)"
-
 
 section "Editor Reactivity"
 
diff -r 108630498c00 -r 72c475e03e22 src/Pure/ML/ml_compiler0.ML
--- a/src/Pure/ML/ml_compiler0.ML	Wed Apr 06 11:50:07 2016 +0200
+++ b/src/Pure/ML/ml_compiler0.ML	Wed Apr 06 11:57:21 2016 +0200
@@ -154,4 +154,4 @@
        ("addPrettyPrinter", "ML_system_pp"),
        ("addOverload", "ML_system_overload")]))
   {debug = false, file = "", line = 0, verbose = false}
-  "open PolyML RunCall";
+  "open PolyML RunCall" handle ERROR _ => ();
diff -r 108630498c00 -r 72c475e03e22 src/Pure/ML/ml_pervasive1.ML
--- a/src/Pure/ML/ml_pervasive1.ML	Wed Apr 06 11:50:07 2016 +0200
+++ b/src/Pure/ML/ml_pervasive1.ML	Wed Apr 06 11:57:21 2016 +0200
@@ -4,11 +4,10 @@
 Pervasive ML environment: final setup.
 *)
 
-if Options.default_bool "ML_system_bootstrap" then ()
-else
-  (List.app ML_Name_Space.forget_structure
-    (remove (op =) "PolyML" ML_Name_Space.bootstrap_structures);
-   ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
+List.app ML_Name_Space.forget_structure
+  (remove (op =) "PolyML" ML_Name_Space.bootstrap_structures);
+
+structure PolyML = struct structure IntInf = PolyML.IntInf end;
 
 Proofterm.proofs := 0;
 
diff -r 108630498c00 -r 72c475e03e22 src/Pure/ROOT1.ML
--- a/src/Pure/ROOT1.ML	Wed Apr 06 11:50:07 2016 +0200
+++ b/src/Pure/ROOT1.ML	Wed Apr 06 11:57:21 2016 +0200
@@ -1,6 +1,6 @@
 (*** Isabelle/Pure bootstrap: final setup ***)
 
 use_thy "Pure";
+use_thy "ML_Root";
 
 use "ML/ml_pervasive1.ML";
-use_thy "ML_Root";