equal
deleted
inserted
replaced
128 Value.map (Inttab.update (id, type_check (name, pos) f (get_value context))) context; |
128 Value.map (Inttab.update (id, type_check (name, pos) f (get_value context))) context; |
129 |
129 |
130 fun map_value f (context as Context.Proof ctxt) = |
130 fun map_value f (context as Context.Proof ctxt) = |
131 let val context' = update_value f context in |
131 let val context' = update_value f context in |
132 if global andalso |
132 if global andalso |
133 Context_Position.is_visible ctxt andalso |
133 Context_Position.is_really_visible ctxt andalso |
134 print_value (get_value (Context.Theory (Context.theory_of context'))) <> |
134 print_value (get_value (Context.Theory (Context.theory_of context'))) <> |
135 print_value (get_value context') |
135 print_value (get_value context') |
136 then |
136 then (warning ("Ignoring local change of global option " ^ quote name); context) |
137 (if Context_Position.is_visible ctxt then |
|
138 warning ("Ignoring local change of global option " ^ quote name) |
|
139 else (); context) |
|
140 else context' |
137 else context' |
141 end |
138 end |
142 | map_value f context = update_value f context; |
139 | map_value f context = update_value f context; |
143 in Config {name = name, pos = pos, get_value = get_value, map_value = map_value} end; |
140 in Config {name = name, pos = pos, get_value = get_value, map_value = map_value} end; |
144 |
141 |