tuned signature;
authorwenzelm
Mon Mar 12 15:31:30 2012 +0100 (2012-03-12)
changeset 46874993c413746f4
parent 46873 7a73f181cbcf
child 46875 162b0c46c559
tuned signature;
src/Provers/classical.ML
src/Pure/context_position.ML
     1.1 --- a/src/Provers/classical.ML	Mon Mar 12 13:53:26 2012 +0100
     1.2 +++ b/src/Provers/classical.ML	Mon Mar 12 15:31:30 2012 +0100
     1.3 @@ -301,9 +301,9 @@
     1.4      error ("Ill-formed destruction rule\n" ^ string_of_thm context th)
     1.5    else Tactic.make_elim th;
     1.6  
     1.7 -fun warn_thm context msg th =
     1.8 -  if (case context of SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt | _ => false)
     1.9 -  then warning (msg ^ string_of_thm context th)
    1.10 +fun warn_thm opt_context msg th =
    1.11 +  if (case opt_context of SOME context => Context_Position.is_visible_proof context | NONE => false)
    1.12 +  then warning (msg ^ string_of_thm opt_context th)
    1.13    else ();
    1.14  
    1.15  fun warn_rules context msg rules th =
     2.1 --- a/src/Pure/context_position.ML	Mon Mar 12 13:53:26 2012 +0100
     2.2 +++ b/src/Pure/context_position.ML	Mon Mar 12 15:31:30 2012 +0100
     2.3 @@ -10,6 +10,7 @@
     2.4    val set_visible: bool -> Proof.context -> Proof.context
     2.5    val restore_visible: Proof.context -> Proof.context -> Proof.context
     2.6    val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
     2.7 +  val is_visible_proof: Context.generic -> bool
     2.8    val if_visible_proof: Context.generic -> ('a -> unit) -> 'a -> unit
     2.9    val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
    2.10    val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
    2.11 @@ -27,8 +28,10 @@
    2.12  
    2.13  fun if_visible ctxt f x = if is_visible ctxt then f x else ();
    2.14  
    2.15 -fun if_visible_proof (Context.Proof ctxt) f x = if_visible ctxt f x
    2.16 -  | if_visible_proof _ _ _ = ();
    2.17 +fun is_visible_proof (Context.Proof ctxt) = is_visible ctxt
    2.18 +  | is_visible_proof _ = false;
    2.19 +
    2.20 +fun if_visible_proof context f x = if is_visible_proof context then f x else ();
    2.21  
    2.22  fun reported_text ctxt pos markup txt =
    2.23    if is_visible ctxt then Position.reported_text pos markup txt else "";