104 val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists |
104 val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists |
105 |
105 |
106 |
106 |
107 (* replaces the official subgoal antiquotation with one *) |
107 (* replaces the official subgoal antiquotation with one *) |
108 (* that is closer to the actual output *) |
108 (* that is closer to the actual output *) |
|
109 fun proof_state state = |
|
110 (case try Toplevel.proof_of state of |
|
111 SOME prf => prf |
|
112 | _ => error "No proof state") |
|
113 |
109 fun output_goals {state = node, ...} _ = |
114 fun output_goals {state = node, ...} _ = |
110 let |
115 let |
111 fun subgoals 0 = "" |
116 fun subgoals 0 = "" |
112 | subgoals 1 = "goal (1 subgoal):" |
117 | subgoals 1 = "goal (1 subgoal):" |
113 | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):" |
118 | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):" |
114 |
119 |
115 fun proof_state state = |
|
116 (case try Toplevel.proof_of state of |
|
117 SOME prf => prf |
|
118 | _ => error "No proof state") |
|
119 |
|
120 val state = proof_state node; |
120 val state = proof_state node; |
121 val goals = Pretty.chunks (Proof.pretty_goals false state); |
121 val goals = Pretty.chunks (Proof.pretty_goals false state); |
122 |
122 |
123 val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd); |
123 val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd); |
124 val (As, B) = Logic.strip_horn prop; |
124 val (As, _) = Logic.strip_horn prop; |
125 val output = (case (length As) of |
125 val output = (case (length As) of |
126 0 => [goals] |
126 0 => [goals] |
127 | n => [Pretty.str (subgoals n), goals]) |
127 | n => [Pretty.str (subgoals n), goals]) |
128 in |
128 in |
129 ThyOutput.output output |
129 ThyOutput.output output |
130 end |
130 end |
131 |
131 |
|
132 fun output_raw_goal_state {state = node, context = ctxt, ...} _ = |
|
133 let |
|
134 val state = proof_state node; |
|
135 val goals = (Proof.get_goal state |> snd |> snd) |
|
136 |
|
137 val output = [Pretty.str (Syntax.string_of_term ctxt (prop_of goals))] |
|
138 val _ = tracing (Syntax.string_of_term ctxt (prop_of goals)) |
|
139 val _ = tracing (Pretty.string_of (Pretty.str (Syntax.string_of_term ctxt (prop_of goals)))) |
|
140 in |
|
141 ThyOutput.output output |
|
142 end |
|
143 |
|
144 |
132 val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals |
145 val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals |
133 |
146 val _ = ThyOutput.antiquotation "raw_goal_state" (Scan.succeed ()) output_raw_goal_state |
|
147 |
134 end; |
148 end; |