1 (* Auxiliary antiquotations for the tutorial. *) |
1 (* Auxiliary antiquotations for the tutorial. *) |
2 |
2 |
3 structure AntiquoteSetup: sig end = |
3 structure AntiquoteSetup = |
4 struct |
4 struct |
5 |
5 |
|
6 open OutputTutorial |
|
7 |
6 (* functions for generating appropriate expressions *) |
8 (* functions for generating appropriate expressions *) |
7 fun ml_val_open (ys, xs) txt = |
9 fun ml_val_open ys xs txt = |
8 let fun ml_val_open_aux ys txt = |
10 let fun ml_val_open_aux ys txt = |
9 "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")"; |
11 "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")"; |
10 in |
12 in |
11 (case xs of |
13 (case xs of |
12 [] => ml_val_open_aux ys txt |
14 [] => ml_val_open_aux ys txt |
13 | _ => ml_val_open_aux ys ("let open " ^ (space_implode " " xs) ^ " in " ^ txt ^ " end")) |
15 | _ => ml_val_open_aux ys ("let open " ^ (space_implode " " xs) ^ " in " ^ txt ^ " end")) |
14 end; |
16 end; |
15 |
17 |
16 fun ml_val txt = ml_val_open ([],[]) txt; |
18 fun ml_val txt = ml_val_open [] [] txt; |
17 |
19 |
18 fun ml_pat (lhs, pat) = |
20 fun ml_pat (lhs, pat) = |
19 let |
21 let |
20 val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat)) |
22 val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat)) |
21 in "val " ^ pat' ^ " = " ^ lhs end; |
23 in "val " ^ pat' ^ " = " ^ lhs end; |
26 (* eval function *) |
28 (* eval function *) |
27 fun eval_fn ctxt exp = |
29 fun eval_fn ctxt exp = |
28 ML_Context.eval_in (SOME ctxt) false Position.none exp |
30 ML_Context.eval_in (SOME ctxt) false Position.none exp |
29 |
31 |
30 (* string functions *) |
32 (* string functions *) |
31 fun string_explode str txt = |
33 fun string_explode prefix_str txt = |
32 map (fn s => str ^ s) (space_explode "\n" txt) |
34 map (fn s => prefix_str ^ s) (split_lines txt) |
33 |
35 |
34 val transform_cmts_str = |
36 val transform_cmts_str = |
35 Source.of_string |
37 Source.of_string |
36 #> ML_Lex.source |
38 #> ML_Lex.source |
37 #> Source.exhaust |
39 #> Source.exhaust |
38 #> Chunks.transform_cmts |
40 #> Chunks.transform_cmts |
39 #> implode |
41 #> implode |
40 #> string_explode ""; |
42 #> string_explode "" |
41 |
|
42 (* output function *) |
|
43 fun output_fn txt = OutputFN.output txt |
|
44 |
43 |
45 (* checks and prints open expressions *) |
44 (* checks and prints open expressions *) |
46 fun output_ml {context = ctxt, ...} (txt, ovars) = |
45 fun output_ml {context = ctxt, ...} (txt, (ovars, structs)) = |
47 (eval_fn ctxt (ml_val_open ovars txt); |
46 (eval_fn ctxt (ml_val_open ovars structs txt); |
48 output_fn (transform_cmts_str txt)) |
47 if structs = [] |
|
48 then output_indexed (transform_cmts_str txt) {main = Code txt, minor = ""} |
|
49 else output_indexed (transform_cmts_str txt) |
|
50 {main = Code txt, minor = ("in {\\tt\\slshape{}" ^ (implode structs) ^ "}")}) |
49 |
51 |
50 val parser_ml = Scan.lift (Args.name -- |
52 val parser_ml = Scan.lift (Args.name -- |
51 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
53 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
52 Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])) |
54 Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])) |
53 |
55 |
54 (* checks and prints types and structures *) |
56 (* checks and prints types and structures *) |
55 fun output_exp ml {context = ctxt, ...} txt = |
57 fun output_struct {context = ctxt, ...} txt = |
56 (eval_fn ctxt (ml txt); |
58 (eval_fn ctxt (ml_struct txt); |
57 output_fn (string_explode "" txt)) |
59 output_indexed (string_explode "" txt) {main = Code txt, minor = "structure"}) |
|
60 |
|
61 fun output_type {context = ctxt, ...} txt = |
|
62 (eval_fn ctxt (ml_type txt); |
|
63 output_indexed (string_explode "" txt) {main = Code txt, minor = "type"}) |
58 |
64 |
59 (* checks and expression agains a result pattern *) |
65 (* checks and expression agains a result pattern *) |
60 fun output_response {context = ctxt, ...} (lhs, pat) = |
66 fun output_response {context = ctxt, ...} (lhs, pat) = |
61 (eval_fn ctxt (ml_pat (lhs, pat)); |
67 (eval_fn ctxt (ml_pat (lhs, pat)); |
62 output_fn ((string_explode "" lhs) @ (string_explode "> " pat))) |
68 output ((string_explode "" lhs) @ (string_explode "> " pat))) |
63 |
69 |
64 (* checks the expressions, but does not check it against a result pattern *) |
70 (* checks the expressions, but does not check it against a result pattern *) |
65 fun output_response_fake {context = ctxt, ...} (lhs, pat) = |
71 fun output_response_fake {context = ctxt, ...} (lhs, pat) = |
66 (eval_fn ctxt (ml_val lhs); |
72 (eval_fn ctxt (ml_val lhs); |
67 output_fn ((string_explode "" lhs) @ (string_explode "> " pat))) |
73 output ((string_explode "" lhs) @ (string_explode "> " pat))) |
68 |
74 |
69 (* checks the expressions, but does not check it against a result pattern *) |
75 (* checks the expressions, but does not check it against a result pattern *) |
70 fun ouput_response_fake_both _ (lhs, pat) = |
76 fun ouput_response_fake_both _ (lhs, pat) = |
71 output_fn ((string_explode "" lhs) @ (string_explode "> " pat)) |
77 output ((string_explode "" lhs) @ (string_explode "> " pat)) |
72 |
78 |
73 val single_arg = Scan.lift (Args.name) |
79 val single_arg = Scan.lift (Args.name) |
74 val two_args = Scan.lift (Args.name -- Args.name) |
80 val two_args = Scan.lift (Args.name -- Args.name) |
75 |
81 |
76 val _ = ThyOutput.antiquotation "ML" parser_ml output_ml |
82 val _ = ThyOutput.antiquotation "ML" parser_ml output_ml |
77 val _ = ThyOutput.antiquotation "ML_type" single_arg (output_exp ml_type) |
83 val _ = ThyOutput.antiquotation "ML_type" single_arg output_type |
78 val _ = ThyOutput.antiquotation "ML_struct" single_arg (output_exp ml_struct) |
84 val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct |
79 val _ = ThyOutput.antiquotation "ML_response" two_args output_response |
85 val _ = ThyOutput.antiquotation "ML_response" two_args output_response |
80 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake |
86 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake |
81 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both |
87 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both |
82 |
88 |
83 fun href_link txt = |
89 fun href_link txt = |