equal
deleted
inserted
replaced
61 outfn {main = Code txt, minor = Plain "structure"} (split_lines txt)) |
61 outfn {main = Code txt, minor = Plain "structure"} (split_lines txt)) |
62 |
62 |
63 val output_struct = gen_output_struct (K output) |
63 val output_struct = gen_output_struct (K output) |
64 val output_struct_ind = gen_output_struct output_indexed |
64 val output_struct_ind = gen_output_struct output_indexed |
65 |
65 |
|
66 (* prints functors; no checks *) |
|
67 fun gen_output_funct outfn {context = ctxt, ...} txt = |
|
68 (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt)) |
|
69 |
|
70 val output_funct = gen_output_funct (K output) |
|
71 val output_funct_ind = gen_output_funct output_indexed |
|
72 |
66 (* checks and prints types *) |
73 (* checks and prints types *) |
67 fun gen_output_type outfn {context = ctxt, ...} txt = |
74 fun gen_output_type outfn {context = ctxt, ...} txt = |
68 (eval_fn ctxt (ml_type txt); |
75 (eval_fn ctxt (ml_type txt); |
69 outfn {main = Code txt, minor = Plain "type"} (split_lines txt)) |
76 outfn {main = Code txt, minor = Plain "type"} (split_lines txt)) |
70 |
77 |
93 val _ = ThyOutput.antiquotation "ML_ind" parser_ml_ind output_ml_ind |
100 val _ = ThyOutput.antiquotation "ML_ind" parser_ml_ind output_ml_ind |
94 val _ = ThyOutput.antiquotation "ML_type" single_arg output_type |
101 val _ = ThyOutput.antiquotation "ML_type" single_arg output_type |
95 val _ = ThyOutput.antiquotation "ML_type_ind" single_arg output_type_ind |
102 val _ = ThyOutput.antiquotation "ML_type_ind" single_arg output_type_ind |
96 val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct |
103 val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct |
97 val _ = ThyOutput.antiquotation "ML_struct_ind" single_arg output_struct_ind |
104 val _ = ThyOutput.antiquotation "ML_struct_ind" single_arg output_struct_ind |
|
105 val _ = ThyOutput.antiquotation "ML_funct" single_arg output_funct |
|
106 val _ = ThyOutput.antiquotation "ML_funct_ind" single_arg output_funct_ind |
98 val _ = ThyOutput.antiquotation "ML_response" two_args output_response |
107 val _ = ThyOutput.antiquotation "ML_response" two_args output_response |
99 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake |
108 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake |
100 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both |
109 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both |
101 |
110 |
102 (* FIXME: experimental *) |
111 (* FIXME: experimental *) |