tuned signature;
authorwenzelm
Thu Jul 18 21:20:09 2013 +0200 (2013-07-18)
changeset 52699abed4121c17e
parent 52698 df1531af559f
child 52700 d63f80f93025
tuned signature;
src/HOL/Tools/SMT/smt_config.ML
src/Provers/classical.ML
src/Pure/context_position.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Thu Jul 18 21:06:21 2013 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Thu Jul 18 21:20:09 2013 +0200
     1.3 @@ -101,9 +101,10 @@
     1.4  fun available_solvers_of ctxt =
     1.5    filter (is_available ctxt) (all_solvers_of ctxt)
     1.6  
     1.7 -fun warn_solver context name =
     1.8 -  Context_Position.if_visible_proof context
     1.9 -    warning ("The SMT solver " ^ quote name ^ " is not installed.")
    1.10 +fun warn_solver (Context.Proof ctxt) name =
    1.11 +      Context_Position.if_visible ctxt
    1.12 +        warning ("The SMT solver " ^ quote name ^ " is not installed.")
    1.13 +  | warn_solver _ _ = ();
    1.14  
    1.15  fun select_solver name context =
    1.16    let
     2.1 --- a/src/Provers/classical.ML	Thu Jul 18 21:06:21 2013 +0200
     2.2 +++ b/src/Provers/classical.ML	Thu Jul 18 21:20:09 2013 +0200
     2.3 @@ -302,10 +302,10 @@
     2.4      error ("Ill-formed destruction rule\n" ^ string_of_thm context th)
     2.5    else Tactic.make_elim th;
     2.6  
     2.7 -fun warn_thm opt_context msg th =
     2.8 -  if (case opt_context of SOME context => Context_Position.is_visible_proof context | NONE => false)
     2.9 -  then warning (msg ^ string_of_thm opt_context th)
    2.10 -  else ();
    2.11 +fun warn_thm (SOME (Context.Proof ctxt)) msg th =
    2.12 +      if Context_Position.is_visible ctxt
    2.13 +      then warning (msg ^ Display.string_of_thm ctxt th) else ()
    2.14 +  | warn_thm _ _ _ = ();
    2.15  
    2.16  fun warn_rules context msg rules th =
    2.17    Item_Net.member rules th andalso (warn_thm context msg th; true);
     3.1 --- a/src/Pure/context_position.ML	Thu Jul 18 21:06:21 2013 +0200
     3.2 +++ b/src/Pure/context_position.ML	Thu Jul 18 21:20:09 2013 +0200
     3.3 @@ -10,8 +10,6 @@
     3.4    val set_visible: bool -> Proof.context -> Proof.context
     3.5    val restore_visible: Proof.context -> Proof.context -> Proof.context
     3.6    val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
     3.7 -  val is_visible_proof: Context.generic -> bool
     3.8 -  val if_visible_proof: Context.generic -> ('a -> unit) -> 'a -> unit
     3.9    val report_generic: Context.generic -> Position.T -> Markup.T -> unit
    3.10    val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
    3.11    val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
    3.12 @@ -38,11 +36,6 @@
    3.13  
    3.14  fun if_visible ctxt f x = if is_visible ctxt then f x else ();
    3.15  
    3.16 -fun is_visible_proof (Context.Proof ctxt) = is_visible ctxt
    3.17 -  | is_visible_proof _ = false;
    3.18 -
    3.19 -fun if_visible_proof context f x = if is_visible_proof context then f x else ();
    3.20 -
    3.21  fun report_generic context pos markup =
    3.22    if is_visible_generic context then
    3.23      Output.report (Position.reported_text pos markup "")