--- a/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML Tue Mar 01 22:11:36 2016 +0100
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML Tue Mar 01 22:49:33 2016 +0100
@@ -184,7 +184,7 @@
in
compiled_rewriter := NONE;
- ML_Compiler0.use_text ML_Env.local_context
+ ML_Compiler0.use_text ML_Env.context
{line = 1, file = "", verbose = false, debug = false} (!buffer);
case !compiled_rewriter of
NONE => raise (Compile "cannot communicate with compiled function")
--- a/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML Tue Mar 01 22:11:36 2016 +0100
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML Tue Mar 01 22:49:33 2016 +0100
@@ -486,7 +486,7 @@
fun writeTextFile name s = File.write (Path.explode name) s
fun use_source src =
- ML_Compiler0.use_text ML_Env.local_context
+ ML_Compiler0.use_text ML_Env.context
{line = 1, file = "", verbose = false, debug = false} src
fun compile rules =
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Mar 01 22:11:36 2016 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Mar 01 22:49:33 2016 +0100
@@ -206,7 +206,7 @@
fun exec verbose code =
ML_Context.exec (fn () =>
- ML_Compiler0.use_text ML_Env.local_context
+ ML_Compiler0.use_text ML_Env.context
{line = 0, file = "generated code", verbose = verbose, debug = false} code)
fun with_overlord_dir name f =
--- a/src/Pure/ML/ml_compiler.ML Tue Mar 01 22:11:36 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML Tue Mar 01 22:49:33 2016 +0100
@@ -149,7 +149,7 @@
fun eval (flags: flags) pos toks =
let
val _ = Secure.deny_ml ();
- val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags};
+ val space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags};
val opt_context = Context.thread_data ();
--- a/src/Pure/ML/ml_env.ML Tue Mar 01 22:11:36 2016 +0100
+++ b/src/Pure/ML/ml_env.ML Tue Mar 01 22:49:33 2016 +0100
@@ -13,9 +13,9 @@
Context.generic -> Context.generic
val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
- val name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
- val local_context: ML_Compiler0.context
- val local_name_space: ML_Name_Space.T
+ val make_name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
+ val context: ML_Compiler0.context
+ val name_space: ML_Name_Space.T
val check_functor: string -> unit
end
@@ -108,7 +108,7 @@
in (val2, type2, fixity2, structure2, signature2, functor2) end);
in make_data (bootstrap, tables', sml_tables', breakpoints) end);
-fun name_space {SML, exchange} : ML_Name_Space.T =
+fun make_name_space {SML, exchange} : ML_Name_Space.T =
let
fun lookup sel1 sel2 name =
if SML then
@@ -162,15 +162,15 @@
allFunct = all #6 #allFunct}
end;
-val local_context: ML_Compiler0.context =
- {name_space = name_space {SML = false, exchange = false},
+val context: ML_Compiler0.context =
+ {name_space = make_name_space {SML = false, exchange = false},
here = Position.here oo Position.line_file,
print = writeln,
error = error};
-val local_name_space = #name_space local_context;
+val name_space = #name_space context;
-val is_functor = is_some o #lookupFunct local_name_space;
+val is_functor = is_some o #lookupFunct name_space;
fun check_functor name =
if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()
--- a/src/Tools/Code/code_runtime.ML Tue Mar 01 22:11:36 2016 +0100
+++ b/src/Tools/Code/code_runtime.ML Tue Mar 01 22:49:33 2016 +0100
@@ -82,7 +82,7 @@
fun exec ctxt verbose code =
(if Config.get ctxt trace then tracing code else ();
ML_Context.exec (fn () =>
- ML_Compiler0.use_text ML_Env.local_context
+ ML_Compiler0.use_text ML_Env.context
{line = 0, file = "generated code", verbose = verbose, debug = false} code));
fun value ctxt (get, put, put_ml) (prelude, value) =
@@ -503,7 +503,7 @@
fun notify_val (string, value) =
let
- val _ = #enterVal ML_Env.local_name_space (string, value);
+ val _ = #enterVal ML_Env.name_space (string, value);
val _ = Theory.setup (Loaded_Values.map (insert (op =) string));
in () end;
@@ -511,27 +511,27 @@
val notifying_context : ML_Compiler0.context =
{name_space =
- {lookupVal = #lookupVal ML_Env.local_name_space,
- lookupType = #lookupType ML_Env.local_name_space,
- lookupFix = #lookupFix ML_Env.local_name_space,
- lookupStruct = #lookupStruct ML_Env.local_name_space,
- lookupSig = #lookupSig ML_Env.local_name_space,
- lookupFunct = #lookupFunct ML_Env.local_name_space,
+ {lookupVal = #lookupVal ML_Env.name_space,
+ lookupType = #lookupType ML_Env.name_space,
+ lookupFix = #lookupFix ML_Env.name_space,
+ lookupStruct = #lookupStruct ML_Env.name_space,
+ lookupSig = #lookupSig ML_Env.name_space,
+ lookupFunct = #lookupFunct ML_Env.name_space,
enterVal = notify_val,
enterType = abort,
enterFix = abort,
enterStruct = abort,
enterSig = abort,
enterFunct = abort,
- allVal = #allVal ML_Env.local_name_space,
- allType = #allType ML_Env.local_name_space,
- allFix = #allFix ML_Env.local_name_space,
- allStruct = #allStruct ML_Env.local_name_space,
- allSig = #allSig ML_Env.local_name_space,
- allFunct = #allFunct ML_Env.local_name_space},
- here = #here ML_Env.local_context,
- print = #print ML_Env.local_context,
- error = #error ML_Env.local_context};
+ allVal = #allVal ML_Env.name_space,
+ allType = #allType ML_Env.name_space,
+ allFix = #allFix ML_Env.name_space,
+ allStruct = #allStruct ML_Env.name_space,
+ allSig = #allSig ML_Env.name_space,
+ allFunct = #allFunct ML_Env.name_space},
+ here = #here ML_Env.context,
+ print = #print ML_Env.context,
+ error = #error ML_Env.context};
in
--- a/src/Tools/Spec_Check/spec_check.ML Tue Mar 01 22:11:36 2016 +0100
+++ b/src/Tools/Spec_Check/spec_check.ML Tue Mar 01 22:49:33 2016 +0100
@@ -128,10 +128,10 @@
let
val return = Unsynchronized.ref "return"
val context : ML_Compiler0.context =
- {name_space = #name_space ML_Env.local_context,
- here = #here ML_Env.local_context,
+ {name_space = #name_space ML_Env.context,
+ here = #here ML_Env.context,
print = fn r => return := r,
- error = #error ML_Env.local_context}
+ error = #error ML_Env.context}
val _ =
Context.setmp_thread_data (SOME (Context.Proof ctxt))
(fn () =>
@@ -145,7 +145,7 @@
fun run_test ctxt s =
Context.setmp_thread_data (SOME (Context.Proof ctxt))
(fn () =>
- ML_Compiler0.use_text ML_Env.local_context
+ ML_Compiler0.use_text ML_Env.context
{line = 0, file = "generated code", verbose = false, debug = false} s) ();
(*split input into tokens*)