src/Pure/context_position.ML

--- a/src/Pure/context_position.ML	Thu Jul 18 21:20:09 2013 +0200
+++ b/src/Pure/context_position.ML	Thu Jul 18 21:57:27 2013 +0200
@@ -7,9 +7,13 @@
 signature CONTEXT_POSITION =
 sig
   val is_visible: Proof.context -> bool
+  val is_visible_global: theory -> bool
+  val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
+  val if_visible_global: theory -> ('a -> unit) -> 'a -> unit
   val set_visible: bool -> Proof.context -> Proof.context
+  val set_visible_global: bool -> theory -> theory
   val restore_visible: Proof.context -> Proof.context -> Proof.context
-  val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
+  val restore_visible_global: theory -> theory -> theory
   val report_generic: Context.generic -> Position.T -> Markup.T -> unit
   val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
   val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
@@ -31,10 +35,16 @@
 
 val is_visible_generic = the_default true o Data.get;
 val is_visible = is_visible_generic o Context.Proof;
-val set_visible = Context.proof_map o Data.put o SOME;
-val restore_visible = set_visible o is_visible;
+val is_visible_global = is_visible_generic o Context.Theory;
 
 fun if_visible ctxt f x = if is_visible ctxt then f x else ();
+fun if_visible_global thy f x = if is_visible_global thy then f x else ();
+
+val set_visible = Context.proof_map o Data.put o SOME;
+val set_visible_global = Context.theory_map o Data.put o SOME;
+
+val restore_visible = set_visible o is_visible;
+val restore_visible_global = set_visible_global o is_visible_global;
 
 fun report_generic context pos markup =
   if is_visible_generic context then