# 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 \structure PolyML = struct structure IntInf = PolyML.IntInf end\); +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";