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