1.1 --- a/src/Pure/Isar/attrib.ML	Mon Aug 04 19:47:25 2014 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Tue Aug 05 11:06:36 2014 +0200
     1.3 @@ -292,7 +292,7 @@
     1.4  in
     1.5  
     1.6  fun partial_evaluation ctxt facts =
     1.7 -  (facts, Context.Proof ctxt) |->
     1.8 +  (facts, Context.Proof (Context_Position.not_really ctxt)) |->
     1.9      fold_map (fn ((b, more_atts), fact) => fn context =>
    1.10        let
    1.11          val (fact', (decls, context')) =

     2.1 --- a/src/Pure/config.ML	Mon Aug 04 19:47:25 2014 +0200
     2.2 +++ b/src/Pure/config.ML	Tue Aug 05 11:06:36 2014 +0200
     2.3 @@ -130,13 +130,10 @@
     2.4      fun map_value f (context as Context.Proof ctxt) =
     2.5            let val context' = update_value f context in
     2.6              if global andalso
     2.7 -              Context_Position.is_visible ctxt andalso
     2.8 +              Context_Position.is_really_visible ctxt andalso
     2.9                print_value (get_value (Context.Theory (Context.theory_of context'))) <>
    2.10                  print_value (get_value context')
    2.11 -            then
    2.12 -             (if Context_Position.is_visible ctxt then
    2.13 -                warning ("Ignoring local change of global option " ^ quote name)
    2.14 -              else (); context)
    2.15 +            then (warning ("Ignoring local change of global option " ^ quote name); context)
    2.16              else context'
    2.17            end
    2.18        | map_value f context = update_value f context;

     3.1 --- a/src/Pure/context_position.ML	Mon Aug 04 19:47:25 2014 +0200
     3.2 +++ b/src/Pure/context_position.ML	Tue Aug 05 11:06:36 2014 +0200
     3.3 @@ -11,6 +11,8 @@
     3.4    val is_visible_global: theory -> bool
     3.5    val set_visible: bool -> Proof.context -> Proof.context
     3.6    val set_visible_global: bool -> theory -> theory
     3.7 +  val is_really_visible: Proof.context -> bool
     3.8 +  val not_really: Proof.context -> Proof.context
     3.9    val restore_visible: Proof.context -> Proof.context -> Proof.context
    3.10    val restore_visible_global: theory -> theory -> theory
    3.11    val is_reported_generic: Context.generic -> Position.T -> bool
    3.12 @@ -28,21 +30,25 @@
    3.13  
    3.14  structure Data = Generic_Data
    3.15  (
    3.16 -  type T = bool option;
    3.17 -  val empty: T = NONE;
    3.18 +  type T = bool option * bool option;  (*really, visible*)
    3.19 +  val empty: T = (NONE, NONE);
    3.20    val extend = I;
    3.21 -  fun merge (x, y): T = if is_some x then x else y;
    3.22 +  fun merge ((a, b), (a', b')) : T = (merge_options (a, a'), merge_options (b, b'));
    3.23  );
    3.24  
    3.25 -val is_visible_generic = the_default true o Data.get;
    3.26 +val is_visible_generic = the_default true o snd o Data.get;
    3.27  val is_visible = is_visible_generic o Context.Proof;
    3.28  val is_visible_global = is_visible_generic o Context.Theory;
    3.29  
    3.30 -val set_visible = Context.proof_map o Data.put o SOME;
    3.31 -val set_visible_global = Context.theory_map o Data.put o SOME;
    3.32 +val set_visible = Context.proof_map o Data.map o apsnd o K o SOME;
    3.33 +val set_visible_global = Context.theory_map o Data.map o apsnd o K o SOME;
    3.34  
    3.35 -val restore_visible = set_visible o is_visible;
    3.36 -val restore_visible_global = set_visible_global o is_visible_global;
    3.37 +val is_really = the_default true o fst o Data.get o Context.Proof;
    3.38 +fun is_really_visible ctxt = is_really ctxt andalso is_visible ctxt;
    3.39 +val not_really = Context.proof_map (Data.map (apfst (K (SOME false))));
    3.40 +
    3.41 +val restore_visible = Context.proof_map o Data.put o Data.get o Context.Proof;
    3.42 +val restore_visible_global = Context.theory_map o Data.put o Data.get o Context.Theory;
    3.43  
    3.44  fun is_reported_generic context pos = is_visible_generic context andalso Position.is_reported pos;
    3.45  fun is_reported ctxt pos = is_visible ctxt andalso Position.is_reported pos;