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 write_file_ml_blk lhs (ProofContext.theory_of ctxt); |
85 output ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
85 output ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
86 |
86 |
87 (* 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 *) |
88 fun output_response_fake {context = ctxt, ...} (lhs, pat) = |
88 fun output_response_fake {context = ctxt, ...} (lhs, pat) = |
89 (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); |
90 write_file_ml_blk lhs (ProofContext.theory_of ctxt); |
91 output ((split_lines lhs) @ (prefix_lines "> " pat))) |
91 output ((split_lines lhs) @ (prefix_lines "> " pat))) |
92 |
92 |
93 (* 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 *) |
94 fun ouput_response_fake_both _ (lhs, pat) = |
94 fun ouput_response_fake_both _ (lhs, pat) = |
95 output ((split_lines lhs) @ (prefix_lines "> " pat)) |
95 output ((split_lines lhs) @ (prefix_lines "> " pat)) |