79 fun output_type_ind {context = ctxt, ...} = gen_output_type (output_indexed ctxt) ctxt |
79 fun output_type_ind {context = ctxt, ...} = gen_output_type (output_indexed ctxt) ctxt |
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 (ProofContext.theory_of ctxt); |
84 write_file_ml_blk lhs (Proof_Context.theory_of ctxt); |
85 output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
85 output ctxt ((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 (ProofContext.theory_of ctxt); |
90 write_file_ml_blk lhs (Proof_Context.theory_of ctxt); |
91 output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))) |
91 output ctxt ((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 {context = ctxt, ...} (lhs, pat) = |
94 fun ouput_response_fake_both {context = ctxt, ...} (lhs, pat) = |
95 output ctxt ((split_lines lhs) @ (prefix_lines "> " pat)) |
95 output ctxt ((split_lines lhs) @ (prefix_lines "> " pat)) |