# HG changeset patch # User wenzelm # Date 1331562690 -3600 # Node ID 993c413746f4e120897f82a06bd662a673bba7d8 # Parent 7a73f181cbcfd53ced00874b57825c629b626a4b tuned signature; diff -r 7a73f181cbcf -r 993c413746f4 src/Provers/classical.ML --- a/src/Provers/classical.ML Mon Mar 12 13:53:26 2012 +0100 +++ b/src/Provers/classical.ML Mon Mar 12 15:31:30 2012 +0100 @@ -301,9 +301,9 @@ error ("Ill-formed destruction rule\n" ^ string_of_thm context th) else Tactic.make_elim th; -fun warn_thm context msg th = - if (case context of SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt | _ => false) - then warning (msg ^ string_of_thm context th) +fun warn_thm opt_context msg th = + if (case opt_context of SOME context => Context_Position.is_visible_proof context | NONE => false) + then warning (msg ^ string_of_thm opt_context th) else (); fun warn_rules context msg rules th = diff -r 7a73f181cbcf -r 993c413746f4 src/Pure/context_position.ML --- a/src/Pure/context_position.ML Mon Mar 12 13:53:26 2012 +0100 +++ b/src/Pure/context_position.ML Mon Mar 12 15:31:30 2012 +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 is_visible_proof: Context.generic -> bool 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 @@ -27,8 +28,10 @@ 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 is_visible_proof (Context.Proof ctxt) = is_visible ctxt + | is_visible_proof _ = false; + +fun if_visible_proof context f x = if is_visible_proof context then f x else (); fun reported_text ctxt pos markup txt = if is_visible ctxt then Position.reported_text pos markup txt else "";