# HG changeset patch
# User boehmes
# Date 1294677705 -3600
# Node ID a45cfc6dfd107e48c3db94e2b4e49afa41a2ba7f
# Parent  3fd79c771ed2b367cedea9aee5b7d39e11b545d0
only print warning in a visible context (previously, the warning was printed more than once)

diff -r 3fd79c771ed2 -r a45cfc6dfd10 src/HOL/Tools/SMT/smt_config.ML
--- 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