src/Tools/Code/code_runtime.ML
changeset 56618 874bdedb2313
parent 56245 84fc7dfa3cd4
child 56920 d651b944c67e
equal deleted inserted replaced
56617:c00646996701 56618:874bdedb2313
   390   fun merge data : T = Library.merge (op =) data
   390   fun merge data : T = Library.merge (op =) data
   391 );
   391 );
   392 
   392 
   393 fun notify_val (string, value) = 
   393 fun notify_val (string, value) = 
   394   let
   394   let
   395     val _ = #enterVal ML_Env.name_space (string, value);
   395     val _ = #enterVal ML_Env.local_name_space (string, value);
   396     val _ = Theory.setup (Loaded_Values.map (insert (op =) string));
   396     val _ = Theory.setup (Loaded_Values.map (insert (op =) string));
   397   in () end;
   397   in () end;
   398 
   398 
   399 fun abort _ = error "Only value bindings allowed.";
   399 fun abort _ = error "Only value bindings allowed.";
   400 
   400 
   401 val notifying_context : use_context =
   401 val notifying_context : use_context =
   402  {tune_source = #tune_source ML_Env.local_context,
   402  {tune_source = #tune_source ML_Env.local_context,
   403   name_space =
   403   name_space =
   404    {lookupVal    = #lookupVal ML_Env.name_space,
   404    {lookupVal    = #lookupVal ML_Env.local_name_space,
   405     lookupType   = #lookupType ML_Env.name_space,
   405     lookupType   = #lookupType ML_Env.local_name_space,
   406     lookupFix    = #lookupFix ML_Env.name_space,
   406     lookupFix    = #lookupFix ML_Env.local_name_space,
   407     lookupStruct = #lookupStruct ML_Env.name_space,
   407     lookupStruct = #lookupStruct ML_Env.local_name_space,
   408     lookupSig    = #lookupSig ML_Env.name_space,
   408     lookupSig    = #lookupSig ML_Env.local_name_space,
   409     lookupFunct  = #lookupFunct ML_Env.name_space,
   409     lookupFunct  = #lookupFunct ML_Env.local_name_space,
   410     enterVal     = notify_val,
   410     enterVal     = notify_val,
   411     enterType    = abort,
   411     enterType    = abort,
   412     enterFix     = abort,
   412     enterFix     = abort,
   413     enterStruct  = abort,
   413     enterStruct  = abort,
   414     enterSig     = abort,
   414     enterSig     = abort,
   415     enterFunct   = abort,
   415     enterFunct   = abort,
   416     allVal       = #allVal ML_Env.name_space,
   416     allVal       = #allVal ML_Env.local_name_space,
   417     allType      = #allType ML_Env.name_space,
   417     allType      = #allType ML_Env.local_name_space,
   418     allFix       = #allFix ML_Env.name_space,
   418     allFix       = #allFix ML_Env.local_name_space,
   419     allStruct    = #allStruct ML_Env.name_space,
   419     allStruct    = #allStruct ML_Env.local_name_space,
   420     allSig       = #allSig ML_Env.name_space,
   420     allSig       = #allSig ML_Env.local_name_space,
   421     allFunct     = #allFunct ML_Env.name_space},
   421     allFunct     = #allFunct ML_Env.local_name_space},
   422   str_of_pos = #str_of_pos ML_Env.local_context,
   422   str_of_pos = #str_of_pos ML_Env.local_context,
   423   print = #print ML_Env.local_context,
   423   print = #print ML_Env.local_context,
   424   error = #error ML_Env.local_context};
   424   error = #error ML_Env.local_context};
   425 
   425 
   426 in
   426 in