src/Pure/context_position.ML

--- a/src/Pure/context_position.ML	Fri Aug 27 18:00:45 2010 +0200
+++ b/src/Pure/context_position.ML	Fri Aug 27 19:43:28 2010 +0200
@@ -9,6 +9,7 @@
   val is_visible: Proof.context -> bool
   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 report_text: Proof.context -> Markup.T -> Position.T -> string -> unit
   val report: Proof.context -> Markup.T -> Position.T -> unit
 end;
@@ -26,6 +27,8 @@
 val set_visible = Data.put;
 val restore_visible = set_visible o is_visible;
 
+fun if_visible ctxt f x = if is_visible ctxt then f x else ();
+
 fun report_text ctxt markup pos txt =
   if is_visible ctxt then Position.report_text markup pos txt else ();