142 |
142 |
143 |
143 |
144 (* replaces the official subgoal antiquotation with one *) |
144 (* replaces the official subgoal antiquotation with one *) |
145 (* that is closer to the actual output *) |
145 (* that is closer to the actual output *) |
146 fun proof_state state = |
146 fun proof_state state = |
147 (case try Toplevel.proof_of state of |
147 (case try (Proof.goal o Toplevel.proof_of) state of |
148 SOME prf => prf |
148 SOME {goal, ...} => goal |
149 | _ => error "No proof state") |
149 | _ => error "No proof state"); |
|
150 |
150 |
151 |
151 fun output_goals {state = node, context = ctxt, ...} _ = |
152 fun output_goals {state = node, context = ctxt, ...} _ = |
152 let |
153 let |
153 fun subgoals 0 = "" |
154 fun subgoals 0 = "" |
154 | subgoals 1 = "goal (1 subgoal):" |
155 | subgoals 1 = "goal (1 subgoal):" |
155 | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):" |
156 | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):" |
156 |
157 |
157 val state = proof_state node; |
158 val state = proof_state node |
158 val goals = Pretty.chunks (Proof.pretty_goals false state); |
159 val goals = Goal_Display.pretty_goal {main = false, limit = false} ctxt state |
159 |
160 |
160 val {prop, ...} = (rep_thm o #goal o Proof.goal) state; |
161 val {prop, ...} = rep_thm state; |
161 val (As, _) = Logic.strip_horn prop; |
162 val (As, _) = Logic.strip_horn prop; |
162 val output = (case (length As) of |
163 val output = (case (length As) of |
163 0 => [goals] |
164 0 => [goals] |
164 | n => [Pretty.str (subgoals n), goals]) |
165 | n => [Pretty.str (subgoals n), goals]) |
165 in |
166 in |
166 Thy_Output.output ctxt output |
167 Thy_Output.output ctxt output |
167 end |
168 end |
168 |
169 |
169 fun output_raw_goal_state {state = node, context = ctxt, ...} _ = |
|
170 let |
|
171 val state = proof_state node; |
|
172 val goals = (#goal o Proof.goal) state; |
|
173 |
170 |
174 val output = [Pretty.str (Syntax.string_of_term ctxt (prop_of goals))] |
171 fun output_raw_goal_state {state, context = ctxt, ...} _ = |
175 val _ = tracing (Syntax.string_of_term ctxt (prop_of goals)) |
172 let |
176 val _ = tracing (Pretty.string_of (Pretty.str (Syntax.string_of_term ctxt (prop_of goals)))) |
173 val goals = proof_state state |
177 in |
174 val output = [Pretty.str (Syntax.string_of_term ctxt (prop_of goals))] |
178 Thy_Output.output ctxt output |
175 in |
179 end |
176 Thy_Output.output ctxt output |
|
177 end |
180 |
178 |
181 val subgoals_setup = |
179 val subgoals_setup = |
182 Thy_Output.antiquotation @{binding "subgoals"} (Scan.succeed ()) output_goals |
180 Thy_Output.antiquotation @{binding "subgoals"} (Scan.succeed ()) output_goals |
183 val raw_goal_state_setup = |
181 val raw_goal_state_setup = |
184 Thy_Output.antiquotation @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state |
182 Thy_Output.antiquotation @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state |