218 fun proof_state state = |
218 fun proof_state state = |
219 (case try (Proof.goal o Toplevel.proof_of) state of |
219 (case try (Proof.goal o Toplevel.proof_of) state of |
220 SOME {goal, ...} => goal |
220 SOME {goal, ...} => goal |
221 | _ => error "No proof state"); |
221 | _ => error "No proof state"); |
222 |
222 |
223 |
|
224 fun output_goals ctxt _ = |
|
225 let |
|
226 fun subgoals 0 = "" |
|
227 | subgoals 1 = "goal (1 subgoal):" |
|
228 | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):" |
|
229 |
|
230 val state = proof_state (Toplevel.presentation_state ctxt) |
|
231 val goals = Goal_Display.pretty_goal ctxt state |
|
232 |
|
233 val prop = Thm.prop_of state; |
|
234 val (As, _) = Logic.strip_horn prop; |
|
235 val out = (case (length As) of |
|
236 0 => goals |
|
237 | n => Pretty.big_list (subgoals n) [goals]) (* FIXME: improve printing? *) |
|
238 in |
|
239 output ctxt [Pretty.string_of out] |
|
240 end |
|
241 |
|
242 |
|
243 fun output_raw_goal_state ctxt _ = |
223 fun output_raw_goal_state ctxt _ = |
244 let |
224 let |
245 val goals = proof_state (Toplevel.presentation_state ctxt) |
225 val goals = proof_state (Toplevel.presentation_state ctxt) |
246 val out = Syntax.string_of_term ctxt (Thm.prop_of goals) |
226 val out = Syntax.string_of_term ctxt (Thm.prop_of goals) |
247 in |
227 in |
248 output ctxt [out] |
228 output ctxt [out] |
249 end |
229 end |
250 |
230 |
251 val subgoals_setup = |
|
252 Thy_Output.antiquotation_raw @{binding "subgoals"} (Scan.succeed ()) output_goals |
|
253 val raw_goal_state_setup = |
231 val raw_goal_state_setup = |
254 Thy_Output.antiquotation_raw @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state |
232 Thy_Output.antiquotation_raw @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state |
255 |
233 |
256 val setup = |
234 val setup = |
257 ml_setup #> |
235 ml_setup #> |
258 ml_file_setup #> |
236 ml_file_setup #> |
259 subgoals_setup #> |
|
260 raw_goal_state_setup |
237 raw_goal_state_setup |
261 end; |
238 end; |