src/Tools/Code/code_runtime.ML
changeset 62495 83db706d7771
parent 62494 b90109b2487c
child 62607 43d282be7350
     1.1 --- a/src/Tools/Code/code_runtime.ML	Tue Mar 01 22:11:36 2016 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Mar 01 22:49:33 2016 +0100
     1.3 @@ -82,7 +82,7 @@
     1.4  fun exec ctxt verbose code =
     1.5   (if Config.get ctxt trace then tracing code else ();
     1.6    ML_Context.exec (fn () =>
     1.7 -    ML_Compiler0.use_text ML_Env.local_context
     1.8 +    ML_Compiler0.use_text ML_Env.context
     1.9        {line = 0, file = "generated code", verbose = verbose, debug = false} code));
    1.10  
    1.11  fun value ctxt (get, put, put_ml) (prelude, value) =
    1.12 @@ -503,7 +503,7 @@
    1.13  
    1.14  fun notify_val (string, value) = 
    1.15    let
    1.16 -    val _ = #enterVal ML_Env.local_name_space (string, value);
    1.17 +    val _ = #enterVal ML_Env.name_space (string, value);
    1.18      val _ = Theory.setup (Loaded_Values.map (insert (op =) string));
    1.19    in () end;
    1.20  
    1.21 @@ -511,27 +511,27 @@
    1.22  
    1.23  val notifying_context : ML_Compiler0.context =
    1.24   {name_space =
    1.25 -   {lookupVal    = #lookupVal ML_Env.local_name_space,
    1.26 -    lookupType   = #lookupType ML_Env.local_name_space,
    1.27 -    lookupFix    = #lookupFix ML_Env.local_name_space,
    1.28 -    lookupStruct = #lookupStruct ML_Env.local_name_space,
    1.29 -    lookupSig    = #lookupSig ML_Env.local_name_space,
    1.30 -    lookupFunct  = #lookupFunct ML_Env.local_name_space,
    1.31 +   {lookupVal    = #lookupVal ML_Env.name_space,
    1.32 +    lookupType   = #lookupType ML_Env.name_space,
    1.33 +    lookupFix    = #lookupFix ML_Env.name_space,
    1.34 +    lookupStruct = #lookupStruct ML_Env.name_space,
    1.35 +    lookupSig    = #lookupSig ML_Env.name_space,
    1.36 +    lookupFunct  = #lookupFunct ML_Env.name_space,
    1.37      enterVal     = notify_val,
    1.38      enterType    = abort,
    1.39      enterFix     = abort,
    1.40      enterStruct  = abort,
    1.41      enterSig     = abort,
    1.42      enterFunct   = abort,
    1.43 -    allVal       = #allVal ML_Env.local_name_space,
    1.44 -    allType      = #allType ML_Env.local_name_space,
    1.45 -    allFix       = #allFix ML_Env.local_name_space,
    1.46 -    allStruct    = #allStruct ML_Env.local_name_space,
    1.47 -    allSig       = #allSig ML_Env.local_name_space,
    1.48 -    allFunct     = #allFunct ML_Env.local_name_space},
    1.49 -  here = #here ML_Env.local_context,
    1.50 -  print = #print ML_Env.local_context,
    1.51 -  error = #error ML_Env.local_context};
    1.52 +    allVal       = #allVal ML_Env.name_space,
    1.53 +    allType      = #allType ML_Env.name_space,
    1.54 +    allFix       = #allFix ML_Env.name_space,
    1.55 +    allStruct    = #allStruct ML_Env.name_space,
    1.56 +    allSig       = #allSig ML_Env.name_space,
    1.57 +    allFunct     = #allFunct ML_Env.name_space},
    1.58 +  here = #here ML_Env.context,
    1.59 +  print = #print ML_Env.context,
    1.60 +  error = #error ML_Env.context};
    1.61  
    1.62  in
    1.63