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 |