1.1 --- a/src/Pure/context_position.ML	Sun Mar 18 12:51:44 2012 +0100
     1.2 +++ b/src/Pure/context_position.ML	Sun Mar 18 13:04:22 2012 +0100
     1.3 @@ -12,6 +12,7 @@
     1.4    val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
     1.5    val is_visible_proof: Context.generic -> bool
     1.6    val if_visible_proof: Context.generic -> ('a -> unit) -> 'a -> unit
     1.7 +  val report_generic: Context.generic -> Position.T -> Markup.T -> unit
     1.8    val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
     1.9    val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
    1.10    val report: Proof.context -> Position.T -> Markup.T -> unit
    1.11 @@ -33,6 +34,11 @@
    1.12  
    1.13  fun if_visible_proof context f x = if is_visible_proof context then f x else ();
    1.14  
    1.15 +fun report_generic context pos markup =
    1.16 +  if Config.get_generic context visible then
    1.17 +    Output.report (Position.reported_text pos markup "")
    1.18 +  else ();
    1.19 +
    1.20  fun reported_text ctxt pos markup txt =
    1.21    if is_visible ctxt then Position.reported_text pos markup txt else "";
    1.22