--- a/src/HOL/Tools/SMT/smt_config.ML Mon Jan 10 17:39:54 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Mon Jan 10 17:41:45 2011 +0100
@@ -98,8 +98,9 @@
fun available_solvers_of ctxt =
filter (is_available ctxt) (all_solvers_of ctxt)
-fun warn_solver name =
- warning ("The SMT solver " ^ quote name ^ " is not installed.")
+fun warn_solver context name =
+ Context_Position.if_visible_proof context
+ warning ("The SMT solver " ^ quote name ^ " is not installed.")
fun select_solver name context =
let
@@ -108,7 +109,8 @@
in
if not (member (op =) (all_solvers_of ctxt) name) then
error ("Trying to select unknown solver: " ^ quote name)
- else if not (is_available ctxt name) then (warn_solver name; upd context)
+ else if not (is_available ctxt name) then
+ (warn_solver context name; upd context)
else upd context
end