# 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;