# HG changeset patch # User wenzelm # Date 1407229596 -7200 # Node ID 39d9c7f175e06f011403a62c89212649ed1ff90f # Parent 4d86378e635ff69bee200e0a0e846fc37261c108 refined context visibility again (amending f5f9fad3321c, 8e3e004f1c31): avoid spurious warning due to global config options; diff -r 4d86378e635f -r 39d9c7f175e0 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Mon Aug 04 19:47:25 2014 +0200 +++ b/src/Pure/Isar/attrib.ML Tue Aug 05 11:06:36 2014 +0200 @@ -292,7 +292,7 @@ in fun partial_evaluation ctxt facts = - (facts, Context.Proof ctxt) |-> + (facts, Context.Proof (Context_Position.not_really ctxt)) |-> fold_map (fn ((b, more_atts), fact) => fn context => let val (fact', (decls, context')) = diff -r 4d86378e635f -r 39d9c7f175e0 src/Pure/config.ML --- a/src/Pure/config.ML Mon Aug 04 19:47:25 2014 +0200 +++ b/src/Pure/config.ML Tue Aug 05 11:06:36 2014 +0200 @@ -130,13 +130,10 @@ 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 + Context_Position.is_really_visible ctxt andalso print_value (get_value (Context.Theory (Context.theory_of context'))) <> print_value (get_value context') - then - (if Context_Position.is_visible ctxt then - warning ("Ignoring local change of global option " ^ quote name) - else (); context) + then (warning ("Ignoring local change of global option " ^ quote name); context) else context' end | map_value f context = update_value f context; diff -r 4d86378e635f -r 39d9c7f175e0 src/Pure/context_position.ML --- a/src/Pure/context_position.ML Mon Aug 04 19:47:25 2014 +0200 +++ b/src/Pure/context_position.ML Tue Aug 05 11:06:36 2014 +0200 @@ -11,6 +11,8 @@ val is_visible_global: theory -> bool val set_visible: bool -> Proof.context -> Proof.context val set_visible_global: bool -> theory -> theory + val is_really_visible: Proof.context -> bool + val not_really: Proof.context -> Proof.context val restore_visible: Proof.context -> Proof.context -> Proof.context val restore_visible_global: theory -> theory -> theory val is_reported_generic: Context.generic -> Position.T -> bool @@ -28,21 +30,25 @@ structure Data = Generic_Data ( - type T = bool option; - val empty: T = NONE; + type T = bool option * bool option; (*really, visible*) + val empty: T = (NONE, NONE); val extend = I; - fun merge (x, y): T = if is_some x then x else y; + fun merge ((a, b), (a', b')) : T = (merge_options (a, a'), merge_options (b, b')); ); -val is_visible_generic = the_default true o Data.get; +val is_visible_generic = the_default true o snd o Data.get; val is_visible = is_visible_generic o Context.Proof; val is_visible_global = is_visible_generic o Context.Theory; -val set_visible = Context.proof_map o Data.put o SOME; -val set_visible_global = Context.theory_map o Data.put o SOME; +val set_visible = Context.proof_map o Data.map o apsnd o K o SOME; +val set_visible_global = Context.theory_map o Data.map o apsnd o K o SOME; -val restore_visible = set_visible o is_visible; -val restore_visible_global = set_visible_global o is_visible_global; +val is_really = the_default true o fst o Data.get o Context.Proof; +fun is_really_visible ctxt = is_really ctxt andalso is_visible ctxt; +val not_really = Context.proof_map (Data.map (apfst (K (SOME false)))); + +val restore_visible = Context.proof_map o Data.put o Data.get o Context.Proof; +val restore_visible_global = Context.theory_map o Data.put o Data.get o Context.Theory; fun is_reported_generic context pos = is_visible_generic context andalso Position.is_reported pos; fun is_reported ctxt pos = is_visible ctxt andalso Position.is_reported pos;