51 |
51 |
52 fun output_ml_response_fake_both ml src ctxt ((lhs,pat),pos) = |
52 fun output_ml_response_fake_both ml src ctxt ((lhs,pat),pos) = |
53 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
53 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
54 in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end |
54 in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end |
55 |
55 |
56 fun check_file_exists ctxt txt = |
56 fun check_file_exists src node = |
57 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () |
57 let |
58 else error ("Source file " ^ quote txt ^ " does not exist.") |
58 fun check txt = |
|
59 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () |
|
60 else error ("Source file " ^ (quote txt) ^ " does not exist.") |
|
61 in |
|
62 ThyOutput.args (Scan.lift Args.name) |
|
63 (ThyOutput.output (fn _ => fn s => (check s; Pretty.str s))) src node |
|
64 end |
59 |
65 |
60 (* to be closer to the actual output *) |
66 (* replaces the official subgoal antiquotation with one *) |
61 fun output_goals main_goal src node = |
67 (* that is closer to the actual output *) |
|
68 fun output_goals src node = |
62 let |
69 let |
63 fun subgoals 0 = "" |
70 fun subgoals 0 = "" |
64 | subgoals 1 = "goal (1 subgoal):" |
71 | subgoals 1 = "goal (1 subgoal):" |
65 | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"; |
72 | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"; |
66 |
73 |
68 (case Option.map Toplevel.proof_node node of |
75 (case Option.map Toplevel.proof_node node of |
69 SOME (SOME prf) => ProofNode.current prf |
76 SOME (SOME prf) => ProofNode.current prf |
70 | _ => error "No proof state"); |
77 | _ => error "No proof state"); |
71 |
78 |
72 val state = proof_state node; |
79 val state = proof_state node; |
73 val goals = Proof.pretty_goals main_goal state; |
80 val goals = Proof.pretty_goals false state; |
74 |
81 |
75 val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd); |
82 val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd); |
76 val (As, B) = Logic.strip_horn prop; |
83 val (As, B) = Logic.strip_horn prop; |
77 val output = (case (length As) of |
84 val output = (case (length As) of |
78 0 => goals |
85 0 => goals |
86 val _ = ThyOutput.add_commands |
93 val _ = ThyOutput.add_commands |
87 [("ML", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- |
94 [("ML", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- |
88 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
95 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
89 Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])))) |
96 Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])))) |
90 (output_ml ml_val_open)), |
97 (output_ml ml_val_open)), |
91 ("ML_file", ThyOutput.args (Scan.lift Args.name) |
98 ("ML_file", check_file_exists), |
92 (ThyOutput.output (fn _ => fn s => (check_file_exists s; Pretty.str s)))), |
|
93 ("ML_text", ThyOutput.args (Scan.lift Args.name) |
|
94 (ThyOutput.output (fn _ => fn s => Pretty.str s))), |
|
95 ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
99 ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
96 (output_ml_response ml_pat)), |
100 (output_ml_response ml_pat)), |
97 ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
101 ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
98 (output_ml_response_fake ml_val)), |
102 (output_ml_response_fake ml_val)), |
99 ("ML_response_fake_both", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
103 ("ML_response_fake_both", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
100 (output_ml_response_fake_both ml_val)), |
104 (output_ml_response_fake_both ml_val)), |
101 ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)), |
105 ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)), |
102 ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type)), |
106 ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type)), |
103 ("subgoals", output_goals false)]; |
107 ("subgoals", output_goals)]; |
104 |
108 |
105 end; |
109 end; |