4 struct |
4 struct |
5 |
5 |
6 open OutputTutorial |
6 open OutputTutorial |
7 |
7 |
8 (* functions for generating appropriate expressions *) |
8 (* functions for generating appropriate expressions *) |
9 fun ml_val_open ys strct txt = |
9 fun ml_val_open ys istruct txt = |
10 let |
10 let |
11 fun ml_val_open_aux ys txt = |
11 fun ml_val_open_aux ys txt = |
12 implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"]; |
12 implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"]; |
13 in |
13 in |
14 (case strct of |
14 (case istruct of |
15 NONE => ml_val_open_aux ys txt |
15 NONE => ml_val_open_aux ys txt |
16 | SOME st => ml_val_open_aux ys ("let open " ^ st ^ " in " ^ txt ^ " end")) |
16 | SOME st => ml_val_open_aux ys ("let open " ^ st ^ " in " ^ txt ^ " end")) |
17 end |
17 end |
18 |
18 |
19 fun ml_val txt = ml_val_open [] NONE txt; |
19 fun ml_val txt = ml_val_open [] NONE txt; |
|
20 fun ml_val_ind istruct txt = ml_val_open [] istruct txt; |
20 |
21 |
21 fun ml_pat (lhs, pat) = |
22 fun ml_pat (lhs, pat) = |
22 let |
23 let |
23 val pat' = implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) |
24 val pat' = implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) |
24 in "val " ^ pat' ^ " = " ^ lhs end; |
25 in "val " ^ pat' ^ " = " ^ lhs end; |
40 #> Source.exhaust |
41 #> Source.exhaust |
41 #> Chunks.transform_cmts |
42 #> Chunks.transform_cmts |
42 #> implode |
43 #> implode |
43 #> string_explode "" |
44 #> string_explode "" |
44 |
45 |
45 (* checks and prints open expressions, calculates index entry *) |
46 (* checks and prints a possibly open expressions, no index *) |
46 fun output_ml {context = ctxt, ...} (txt, (ovars, istruc)) = |
47 fun output_ml {context = ctxt, ...} (txt, (ovars, istruc)) = |
47 (eval_fn ctxt (ml_val_open ovars istruc txt); |
48 (eval_fn ctxt (ml_val_open ovars istruc txt); output (string_explode "" txt)) |
|
49 |
|
50 val parser_ml = Scan.lift (Args.name -- |
|
51 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
|
52 Scan.option (Args.$$$ "in" |-- OuterParse.!!! Args.name))) |
|
53 |
|
54 (* checks and prinds a single entity, with index *) |
|
55 fun output_ml_ind {context = ctxt, ...} (txt, istruc) = |
|
56 (eval_fn ctxt (ml_val_ind istruc txt); |
48 case (istruc, Long_Name.base_name txt, Long_Name.qualifier txt) of |
57 case (istruc, Long_Name.base_name txt, Long_Name.qualifier txt) of |
49 (NONE, bn, "") => output_indexed (transform_cmts_str txt) {main = Code txt, minor = NoString} |
58 (NONE, bn, "") => output_indexed (transform_cmts_str txt) {main = Code txt, minor = NoString} |
50 | (NONE, bn, qn) => output_indexed (transform_cmts_str txt) {main = Code bn, minor = IStruct qn} |
59 | (NONE, bn, qn) => output_indexed (transform_cmts_str txt) {main = Code bn, minor = IStruct qn} |
51 | (SOME st, _, _) => output_indexed (transform_cmts_str txt) {main = Code txt, minor = IStruct st}) |
60 | (SOME st, _, _) => output_indexed (transform_cmts_str txt) {main = Code txt, minor = IStruct st}) |
52 |
61 |
53 val parser_ml = Scan.lift (Args.name -- |
62 val parser_ml_ind = Scan.lift (Args.name -- |
54 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
63 Scan.option (Args.$$$ "in" |-- OuterParse.!!! Args.name)) |
55 Scan.option (Args.$$$ "in" |-- OuterParse.!!! Args.name))) |
|
56 |
64 |
57 (* checks and prints types and structures *) |
65 (* checks and prints types and structures *) |
58 fun output_struct {context = ctxt, ...} txt = |
66 fun output_struct {context = ctxt, ...} txt = |
59 (eval_fn ctxt (ml_struct txt); |
67 (eval_fn ctxt (ml_struct txt); |
60 output_indexed (string_explode "" txt) {main = Code txt, minor = Plain "structure"}) |
68 output_indexed (string_explode "" txt) {main = Code txt, minor = Plain "structure"}) |
79 |
87 |
80 val single_arg = Scan.lift (Args.name) |
88 val single_arg = Scan.lift (Args.name) |
81 val two_args = Scan.lift (Args.name -- Args.name) |
89 val two_args = Scan.lift (Args.name -- Args.name) |
82 |
90 |
83 val _ = ThyOutput.antiquotation "ML" parser_ml output_ml |
91 val _ = ThyOutput.antiquotation "ML" parser_ml output_ml |
|
92 val _ = ThyOutput.antiquotation "ML_ind" parser_ml_ind output_ml_ind |
84 val _ = ThyOutput.antiquotation "ML_type" single_arg output_type |
93 val _ = ThyOutput.antiquotation "ML_type" single_arg output_type |
85 val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct |
94 val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct |
86 val _ = ThyOutput.antiquotation "ML_response" two_args output_response |
95 val _ = ThyOutput.antiquotation "ML_response" two_args output_response |
87 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake |
96 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake |
88 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both |
97 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both |