55 |
55 |
56 fun check_file_exists ctxt txt = |
56 fun check_file_exists ctxt txt = |
57 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () |
57 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () |
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 *) |
|
61 fun output_goals main_goal src node = |
|
62 let |
|
63 fun subgoals 0 = "No subgoals!" |
|
64 | subgoals 1 = "goal (1 subgoal):" |
|
65 | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"; |
|
66 |
|
67 fun proof_state node = |
|
68 (case Option.map Toplevel.proof_node node of |
|
69 SOME (SOME prf) => ProofNode.current prf |
|
70 | _ => error "No proof state"); |
|
71 |
|
72 val state = proof_state node |
|
73 val goals = Proof.pretty_goals main_goal state; |
|
74 val msg = Pretty.str (subgoals (length goals)) |
|
75 in |
|
76 ThyOutput.args (Scan.succeed ()) |
|
77 (Chunks.output (fn _ => fn _ => Pretty.chunks (msg::goals))) src node |
|
78 end |
|
79 |
|
80 |
60 val _ = ThyOutput.add_commands |
81 val _ = ThyOutput.add_commands |
61 [("ML", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- |
82 [("ML", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- |
62 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
83 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
63 Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])))) |
84 Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])))) |
64 (output_ml ml_val_open)), |
85 (output_ml ml_val_open)), |
71 ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
92 ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
72 (output_ml_response_fake ml_val)), |
93 (output_ml_response_fake ml_val)), |
73 ("ML_response_fake_both", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
94 ("ML_response_fake_both", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
74 (output_ml_response_fake_both ml_val)), |
95 (output_ml_response_fake_both ml_val)), |
75 ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)), |
96 ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)), |
76 ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type))]; |
97 ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type)), |
|
98 ("subgoals", output_goals false)]; |
77 |
99 |
78 end; |
100 end; |