28 fun ml_struct txt = |
28 fun ml_struct txt = |
29 implode ["functor DUMMY_FUNCTOR() = struct structure DUMMY = ", txt, " end"] |
29 implode ["functor DUMMY_FUNCTOR() = struct structure DUMMY = ", txt, " end"] |
30 |
30 |
31 fun ml_type txt = |
31 fun ml_type txt = |
32 implode ["val _ = NONE : (", txt, ") option"]; |
32 implode ["val _ = NONE : (", txt, ") option"]; |
|
33 |
|
34 fun ml_out txt = |
|
35 implode ["val _ = Pretty.writeln ((Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation ((", txt, "), ML_Options.get_print_depth ()))))) handle _ => writeln \"exception\""] |
33 |
36 |
34 (* eval function *) |
37 (* eval function *) |
35 fun eval_fn ctxt exp = |
38 fun eval_fn ctxt exp = |
36 ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags |
39 ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags |
37 {delimited = false, text = exp, pos = Position.none} |
40 {delimited = false, text = exp, pos = Position.none} |
80 fun output_type_ind {context = ctxt, ...} = gen_output_type (output_indexed ctxt) ctxt |
83 fun output_type_ind {context = ctxt, ...} = gen_output_type (output_indexed ctxt) ctxt |
81 |
84 |
82 (* checks and expression agains a result pattern *) |
85 (* checks and expression agains a result pattern *) |
83 fun output_response {context = ctxt, ...} (lhs, pat) = |
86 fun output_response {context = ctxt, ...} (lhs, pat) = |
84 (eval_fn ctxt (ml_pat (lhs, pat)); |
87 (eval_fn ctxt (ml_pat (lhs, pat)); |
85 (*write_file_ml_blk lhs (Proof_Context.theory_of ctxt);*) |
88 eval_fn ctxt (ml_out lhs); |
86 output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
89 output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
87 |
90 |
88 (* checks the expressions, but does not check it against a result pattern *) |
91 (* checks the expressions, but does not check it against a result pattern *) |
89 fun output_response_fake {context = ctxt, ...} (lhs, pat) = |
92 fun output_response_fake {context = ctxt, ...} (lhs, pat) = |
90 (eval_fn ctxt (ml_val [] NONE lhs); |
93 (eval_fn ctxt (ml_val [] NONE lhs); |
91 (*write_file_ml_blk lhs (Proof_Context.theory_of ctxt);*) |
94 eval_fn ctxt (ml_out lhs); |
92 output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))) |
95 output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))) |
93 |
96 |
94 (* checks the expressions, but does not check it against a result pattern *) |
97 (* checks the expressions, but does not check it against a result pattern *) |
95 fun ouput_response_fake_both {context = ctxt, ...} (lhs, pat) = |
98 fun ouput_response_fake_both {context = ctxt, ...} (lhs, pat) = |
96 output ctxt ((split_lines lhs) @ (prefix_lines "> " pat)) |
99 (output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))) |
97 |
100 |
98 val single_arg = Scan.lift (Args.name) |
101 val single_arg = Scan.lift (Args.name) |
99 val two_args = Scan.lift (Args.name -- Args.name) |
102 val two_args = Scan.lift (Args.name -- Args.name) |
100 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) |
103 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) |
101 |
104 |