--- a/src/Pure/config.ML Fri Apr 27 21:44:44 2012 +0200
+++ b/src/Pure/config.ML Fri Apr 27 21:47:47 2012 +0200
@@ -121,12 +121,15 @@
fun update_value f context =
Value.map (Inttab.update (id, type_check name f (get_value context))) context;
- fun map_value f (context as Context.Proof _) =
+ fun map_value f (context as Context.Proof ctxt) =
let val context' = update_value f context in
if global andalso
+ Context_Position.is_visible ctxt andalso
print_value (get_value (Context.Theory (Context.theory_of context'))) <>
print_value (get_value context')
- then (warning ("Ignoring local change of global option " ^ quote name); context)
+ then
+ (Context_Position.if_visible ctxt warning
+ ("Ignoring local change of global option " ^ quote name); context)
else context'
end
| map_value f context = update_value f context;