equal
deleted
inserted
replaced
99 | NONE => false) |
99 | NONE => false) |
100 |
100 |
101 fun available_solvers_of ctxt = |
101 fun available_solvers_of ctxt = |
102 filter (is_available ctxt) (all_solvers_of ctxt) |
102 filter (is_available ctxt) (all_solvers_of ctxt) |
103 |
103 |
104 fun warn_solver context name = |
104 fun warn_solver (Context.Proof ctxt) name = |
105 Context_Position.if_visible_proof context |
105 Context_Position.if_visible ctxt |
106 warning ("The SMT solver " ^ quote name ^ " is not installed.") |
106 warning ("The SMT solver " ^ quote name ^ " is not installed.") |
|
107 | warn_solver _ _ = (); |
107 |
108 |
108 fun select_solver name context = |
109 fun select_solver name context = |
109 let |
110 let |
110 val ctxt = Context.proof_of context |
111 val ctxt = Context.proof_of context |
111 val upd = Solvers.map (apsnd (K (SOME name))) |
112 val upd = Solvers.map (apsnd (K (SOME name))) |