equal
deleted
inserted
replaced
96 | NONE => false) |
96 | NONE => false) |
97 |
97 |
98 fun available_solvers_of ctxt = |
98 fun available_solvers_of ctxt = |
99 filter (is_available ctxt) (all_solvers_of ctxt) |
99 filter (is_available ctxt) (all_solvers_of ctxt) |
100 |
100 |
101 fun warn_solver name = |
101 fun warn_solver context name = |
102 warning ("The SMT solver " ^ quote name ^ " is not installed.") |
102 Context_Position.if_visible_proof context |
|
103 warning ("The SMT solver " ^ quote name ^ " is not installed.") |
103 |
104 |
104 fun select_solver name context = |
105 fun select_solver name context = |
105 let |
106 let |
106 val ctxt = Context.proof_of context |
107 val ctxt = Context.proof_of context |
107 val upd = Solvers.map (apsnd (K (SOME name))) |
108 val upd = Solvers.map (apsnd (K (SOME name))) |
108 in |
109 in |
109 if not (member (op =) (all_solvers_of ctxt) name) then |
110 if not (member (op =) (all_solvers_of ctxt) name) then |
110 error ("Trying to select unknown solver: " ^ quote name) |
111 error ("Trying to select unknown solver: " ^ quote name) |
111 else if not (is_available ctxt name) then (warn_solver name; upd context) |
112 else if not (is_available ctxt name) then |
|
113 (warn_solver context name; upd context) |
112 else upd context |
114 else upd context |
113 end |
115 end |
114 |
116 |
115 fun no_solver_err () = error "No SMT solver selected" |
117 fun no_solver_err () = error "No SMT solver selected" |
116 |
118 |