equal
deleted
inserted
replaced
91 val success = rc = 0 andalso is_none failure |
91 val success = rc = 0 andalso is_none failure |
92 val message = |
92 val message = |
93 if is_some failure then "External prover failed." |
93 if is_some failure then "External prover failed." |
94 else if rc <> 0 then "External prover failed: " ^ proof |
94 else if rc <> 0 then "External prover failed: " ^ proof |
95 else "Try this command: " ^ produce_answer name (proof, thm_names, ctxt, th, subgoalno) |
95 else "Try this command: " ^ produce_answer name (proof, thm_names, ctxt, th, subgoalno) |
96 |
96 val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof) |
97 val _ = |
|
98 if is_some failure |
|
99 then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof) |
|
100 else () |
|
101 val _ = |
|
102 if rc <> 0 |
|
103 then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof) |
|
104 else () |
|
105 in (success, message, proof, thm_names, the_const_counts) end; |
97 in (success, message, proof, thm_names, the_const_counts) end; |
106 |
98 |
107 |
99 |
108 |
100 |
109 (** common provers **) |
101 (** common provers **) |