added Context_Position.is_visible_proof, which treats a global theory as invisible (unlike the default);

--- a/src/Pure/context_position.ML	Sat Jan 08 14:30:54 2011 +0100
+++ b/src/Pure/context_position.ML	Sat Jan 08 14:32:55 2011 +0100
@@ -10,6 +10,7 @@
   val set_visible: bool -> Proof.context -> Proof.context
   val restore_visible: Proof.context -> Proof.context -> Proof.context
   val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
+  val if_visible_proof: Context.generic -> ('a -> unit) -> 'a -> unit
   val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
   val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
   val report: Proof.context -> Position.T -> Markup.T -> unit
@@ -25,6 +26,9 @@
 
 fun if_visible ctxt f x = if is_visible ctxt then f x else ();
 
+fun if_visible_proof (Context.Proof ctxt) f x = if_visible ctxt f x
+  | if_visible_proof _ _ _ = ();
+
 fun reported_text ctxt pos markup txt =
   if is_visible ctxt then Position.reported_text pos markup txt else "";