equal
deleted
inserted
replaced
109 (case try Toplevel.proof_of state of |
109 (case try Toplevel.proof_of state of |
110 SOME prf => prf |
110 SOME prf => prf |
111 | _ => error "No proof state") |
111 | _ => error "No proof state") |
112 |
112 |
113 val state = proof_state node; |
113 val state = proof_state node; |
114 val goals = Proof.pretty_goals false state; |
114 val goals = Pretty.chunks (Proof.pretty_goals false state); |
115 |
115 |
116 val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd); |
116 val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd); |
117 val (As, B) = Logic.strip_horn prop; |
117 val (As, B) = Logic.strip_horn prop; |
118 val output = (case (length As) of |
118 val output = (case (length As) of |
119 0 => goals |
119 0 => [goals] |
120 | n => (Pretty.str (subgoals n))::goals) |
120 | n => [Pretty.str (subgoals n), goals]) |
121 in |
121 in |
122 ThyOutput.output output |
122 ThyOutput.output output |
123 end |
123 end |
124 |
124 |
125 |
|
126 val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals |
125 val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals |
127 |
126 |
128 end; |
127 end; |