58 else error ("Source file " ^ quote txt ^ " does not exist.") |
58 else error ("Source file " ^ quote txt ^ " does not exist.") |
59 |
59 |
60 (* to be closer to the actual output *) |
60 (* to be closer to the actual output *) |
61 fun output_goals main_goal src node = |
61 fun output_goals main_goal src node = |
62 let |
62 let |
63 fun subgoals 0 = "No subgoals!" |
63 fun subgoals 0 = "" |
64 | subgoals 1 = "goal (1 subgoal):" |
64 | subgoals 1 = "goal (1 subgoal):" |
65 | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"; |
65 | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"; |
66 |
66 |
67 fun proof_state node = |
67 fun proof_state node = |
68 (case Option.map Toplevel.proof_node node of |
68 (case Option.map Toplevel.proof_node node of |
69 SOME (SOME prf) => ProofNode.current prf |
69 SOME (SOME prf) => ProofNode.current prf |
70 | _ => error "No proof state"); |
70 | _ => error "No proof state"); |
71 |
71 |
72 val state = proof_state node |
72 val state = proof_state node; |
73 val goals = Proof.pretty_goals main_goal state; |
73 val goals = Proof.pretty_goals main_goal state; |
74 val msg = Pretty.str (subgoals (length goals)) |
74 |
|
75 val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd); |
|
76 val (As, B) = Logic.strip_horn prop; |
|
77 val output = (case (length As) of |
|
78 0 => goals |
|
79 | n => (Pretty.str (subgoals n))::goals) |
75 in |
80 in |
76 ThyOutput.args (Scan.succeed ()) |
81 ThyOutput.args (Scan.succeed ()) |
77 (Chunks.output (fn _ => fn _ => Pretty.chunks (msg::goals))) src node |
82 (Chunks.output (fn _ => fn _ => Pretty.chunks output)) src node |
78 end |
83 end |
79 |
84 |
80 |
85 |
81 val _ = ThyOutput.add_commands |
86 val _ = ThyOutput.add_commands |
82 [("ML", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- |
87 [("ML", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- |