79 val output_type_ind = gen_output_type output_indexed |
79 val output_type_ind = gen_output_type output_indexed |
80 |
80 |
81 (* checks and expression agains a result pattern *) |
81 (* checks and expression agains a result pattern *) |
82 fun output_response {context = ctxt, ...} (lhs, pat) = |
82 fun output_response {context = ctxt, ...} (lhs, pat) = |
83 (eval_fn ctxt (ml_pat (lhs, pat)); |
83 (eval_fn ctxt (ml_pat (lhs, pat)); |
|
84 write_file_ml_blk lhs (Context.theory_of_proof ctxt); |
84 output ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
85 output ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
85 |
86 |
86 (* checks the expressions, but does not check it against a result pattern *) |
87 (* checks the expressions, but does not check it against a result pattern *) |
87 fun output_response_fake {context = ctxt, ...} (lhs, pat) = |
88 fun output_response_fake {context = ctxt, ...} (lhs, pat) = |
88 (eval_fn ctxt (ml_val [] NONE lhs); |
89 (eval_fn ctxt (ml_val [] NONE lhs); |
|
90 write_file_ml_blk lhs (Context.theory_of_proof ctxt); |
89 output ((split_lines lhs) @ (prefix_lines "> " pat))) |
91 output ((split_lines lhs) @ (prefix_lines "> " pat))) |
90 |
92 |
91 (* checks the expressions, but does not check it against a result pattern *) |
93 (* checks the expressions, but does not check it against a result pattern *) |
92 fun ouput_response_fake_both _ (lhs, pat) = |
94 fun ouput_response_fake_both _ (lhs, pat) = |
93 output ((split_lines lhs) @ (prefix_lines "> " pat)) |
95 output ((split_lines lhs) @ (prefix_lines "> " pat)) |