equal
deleted
inserted
replaced
99 |
99 |
100 fun available_solvers_of ctxt = |
100 fun available_solvers_of ctxt = |
101 filter (is_available ctxt) (all_solvers_of ctxt) |
101 filter (is_available ctxt) (all_solvers_of ctxt) |
102 |
102 |
103 fun warn_solver (Context.Proof ctxt) name = |
103 fun warn_solver (Context.Proof ctxt) name = |
104 Context_Position.if_visible ctxt |
104 if Context_Position.is_visible ctxt then |
105 warning ("The SMT solver " ^ quote name ^ " is not installed.") |
105 warning ("The SMT solver " ^ quote name ^ " is not installed.") |
|
106 else () |
106 | warn_solver _ _ = (); |
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 |