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 istruct txt = |
9 fun translate_string f str = |
10 let |
10 implode (map f (Symbol.explode str)) |
11 fun ml_val_open_aux ys txt = |
|
12 implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"]; |
|
13 in |
|
14 (case istruct of |
|
15 NONE => ml_val_open_aux ys txt |
|
16 | SOME st => ml_val_open_aux ys ("let open " ^ st ^ " in " ^ txt ^ " end")) |
|
17 end |
|
18 |
11 |
19 fun ml_val txt = ml_val_open [] NONE txt; |
12 fun prefix_lines prfx txt = |
20 fun ml_val_ind istruct txt = ml_val_open [] istruct txt; |
13 map (fn s => prfx ^ s) (split_lines txt) |
|
14 |
|
15 fun ml_with_vars ys txt = |
|
16 implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"] |
|
17 |
|
18 fun ml_with_struct (NONE) txt = txt |
|
19 | ml_with_struct (SOME st) txt = implode ["let open ", st, " in ", txt, " end"] |
|
20 |
|
21 fun ml_val vs stru txt = |
|
22 txt |> ml_with_struct stru |
|
23 |> ml_with_vars vs |
21 |
24 |
22 fun ml_pat (lhs, pat) = |
25 fun ml_pat (lhs, pat) = |
23 let |
26 implode ["val ", translate_string (fn "\<dots>" => "_" | s => s) pat, " = ", lhs] |
24 val pat' = implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) |
|
25 in "val " ^ pat' ^ " = " ^ lhs end; |
|
26 |
27 |
27 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end"; |
28 fun ml_struct txt = |
28 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option"; |
29 implode ["functor DUMMY_FUNCTOR() = struct structure DUMMY = ", txt, " end"] |
|
30 |
|
31 fun ml_type txt = |
|
32 implode ["val _ = NONE : (", txt, ") option"]; |
29 |
33 |
30 (* eval function *) |
34 (* eval function *) |
31 fun eval_fn ctxt exp = |
35 fun eval_fn ctxt exp = |
32 ML_Context.eval_in (SOME ctxt) false Position.none exp |
36 ML_Context.eval_in (SOME ctxt) false Position.none exp |
33 |
37 |
34 (* string functions *) |
|
35 fun string_explode prefix_str txt = |
|
36 map (fn s => prefix_str ^ s) (split_lines txt) |
|
37 |
|
38 val transform_cmts_str = |
|
39 Source.of_string |
|
40 #> ML_Lex.source |
|
41 #> Source.exhaust |
|
42 #> Chunks.transform_cmts |
|
43 #> implode |
|
44 #> string_explode "" |
|
45 |
|
46 (* checks and prints a possibly open expressions, no index *) |
38 (* checks and prints a possibly open expressions, no index *) |
47 fun output_ml {context = ctxt, ...} (txt, (ovars, istruc)) = |
39 fun output_ml {context = ctxt, ...} (txt, (vs, stru)) = |
48 (eval_fn ctxt (ml_val_open ovars istruc txt); output (string_explode "" txt)) |
40 (eval_fn ctxt (ml_val vs stru txt); |
|
41 output (split_lines txt)) |
49 |
42 |
50 val parser_ml = Scan.lift (Args.name -- |
43 val parser_ml = Scan.lift (Args.name -- |
51 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
44 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
52 Scan.option (Args.$$$ "in" |-- OuterParse.!!! Args.name))) |
45 Scan.option (Args.$$$ "in" |-- OuterParse.!!! Args.name))) |
53 |
46 |
54 (* checks and prinds a single entity, with index *) |
47 (* checks and prints a single ML-item and produces an index entry *) |
55 fun output_ml_ind {context = ctxt, ...} (txt, istruc) = |
48 fun output_ml_ind {context = ctxt, ...} (txt, stru) = |
56 (eval_fn ctxt (ml_val_ind istruc txt); |
49 (eval_fn ctxt (ml_val [] stru txt); |
57 case (istruc, Long_Name.base_name txt, Long_Name.qualifier txt) of |
50 case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of |
58 (NONE, bn, "") => output_indexed (transform_cmts_str txt) {main = Code txt, minor = NoString} |
51 (NONE, bn, "") => output_indexed {main = Code txt, minor = NoString} (split_lines txt) |
59 | (NONE, bn, qn) => output_indexed (transform_cmts_str txt) {main = Code bn, minor = IStruct qn} |
52 | (NONE, bn, qn) => output_indexed {main = Code bn, minor = Struct qn} (split_lines txt) |
60 | (SOME st, _, _) => output_indexed (transform_cmts_str txt) {main = Code txt, minor = IStruct st}) |
53 | (SOME st, _, _) => output_indexed {main = Code txt, minor = Struct st} (split_lines txt)) |
61 |
54 |
62 val parser_ml_ind = Scan.lift (Args.name -- |
55 val parser_ml_ind = Scan.lift (Args.name -- |
63 Scan.option (Args.$$$ "in" |-- OuterParse.!!! Args.name)) |
56 Scan.option (Args.$$$ "in" |-- OuterParse.!!! Args.name)) |
64 |
57 |
65 (* checks and prints types and structures *) |
58 (* checks and prints structures *) |
66 fun output_struct {context = ctxt, ...} txt = |
59 fun gen_output_struct outfn {context = ctxt, ...} txt = |
67 (eval_fn ctxt (ml_struct txt); |
60 (eval_fn ctxt (ml_struct txt); |
68 output_indexed (string_explode "" txt) {main = Code txt, minor = Plain "structure"}) |
61 outfn {main = Code txt, minor = Plain "structure"} (split_lines txt)) |
69 |
62 |
70 fun output_type {context = ctxt, ...} txt = |
63 val output_struct = gen_output_struct (K output) |
71 (eval_fn ctxt (ml_type txt); |
64 val output_struct_ind = gen_output_struct output_indexed |
72 output_indexed (string_explode "" txt) {main = Code txt, minor = Plain "type"}) |
65 |
|
66 (* checks and prints types *) |
|
67 fun gen_output_type outfn {context = ctxt, ...} txt = |
|
68 (eval_fn ctxt (ml_type txt); |
|
69 outfn {main = Code txt, minor = Plain "type"} (split_lines txt)) |
|
70 |
|
71 val output_type = gen_output_type (K output) |
|
72 val output_type_ind = gen_output_type output_indexed |
73 |
73 |
74 (* checks and expression agains a result pattern *) |
74 (* checks and expression agains a result pattern *) |
75 fun output_response {context = ctxt, ...} (lhs, pat) = |
75 fun output_response {context = ctxt, ...} (lhs, pat) = |
76 (eval_fn ctxt (ml_pat (lhs, pat)); |
76 (eval_fn ctxt (ml_pat (lhs, pat)); |
77 output ((string_explode "" lhs) @ (string_explode "> " pat))) |
77 output ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
78 |
78 |
79 (* checks the expressions, but does not check it against a result pattern *) |
79 (* checks the expressions, but does not check it against a result pattern *) |
80 fun output_response_fake {context = ctxt, ...} (lhs, pat) = |
80 fun output_response_fake {context = ctxt, ...} (lhs, pat) = |
81 (eval_fn ctxt (ml_val lhs); |
81 (eval_fn ctxt (ml_val [] NONE lhs); |
82 output ((string_explode "" lhs) @ (string_explode "> " pat))) |
82 output ((split_lines lhs) @ (prefix_lines "> " pat))) |
83 |
83 |
84 (* checks the expressions, but does not check it against a result pattern *) |
84 (* checks the expressions, but does not check it against a result pattern *) |
85 fun ouput_response_fake_both _ (lhs, pat) = |
85 fun ouput_response_fake_both _ (lhs, pat) = |
86 output ((string_explode "" lhs) @ (string_explode "> " pat)) |
86 output ((split_lines lhs) @ (prefix_lines "> " pat)) |
87 |
87 |
88 val single_arg = Scan.lift (Args.name) |
88 val single_arg = Scan.lift (Args.name) |
89 val two_args = Scan.lift (Args.name -- Args.name) |
89 val two_args = Scan.lift (Args.name -- Args.name) |
90 |
90 |
91 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 |
92 val _ = ThyOutput.antiquotation "ML_ind" parser_ml_ind output_ml_ind |
93 val _ = ThyOutput.antiquotation "ML_type" single_arg output_type |
93 val _ = ThyOutput.antiquotation "ML_type" single_arg output_type |
|
94 val _ = ThyOutput.antiquotation "ML_type_ind" single_arg output_type_ind |
94 val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct |
95 val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct |
|
96 val _ = ThyOutput.antiquotation "ML_struct_ind" single_arg output_struct_ind |
95 val _ = ThyOutput.antiquotation "ML_response" two_args output_response |
97 val _ = ThyOutput.antiquotation "ML_response" two_args output_response |
96 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake |
98 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake |
97 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both |
99 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both |
98 |
100 |
99 fun href_link txt = |
101 fun href_link txt = |
100 let |
102 let |
101 val raw = Symbol.encode_raw |
103 val raw = Symbol.encode_raw |
102 val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/" |
104 val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/" |
103 in |
105 in |
104 (raw "\\href{") ^ (raw path) ^ (raw txt) ^ (raw "}{") ^ txt ^ (raw "}") |
106 implode [raw "\\href{", raw path, raw txt, raw "}{", txt, raw "}"] |
105 end |
107 end |
106 |
108 |
107 (* checks whether a file exists in the Isabelle distribution *) |
109 (* checks whether a file exists in the Isabelle distribution *) |
108 fun check_file_exists _ txt = |
110 fun check_file_exists _ txt = |
109 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
111 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
110 then output [href_link txt] |
112 then output [href_link txt] |
111 else error ("Source file " ^ (quote txt) ^ " does not exist.")) |
113 else error (implode ["Source file ", quote txt, " does not exist."])) |
|
114 |
112 |
115 |
113 val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists |
116 val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists |
114 |
117 |
115 |
118 |
116 (* replaces the official subgoal antiquotation with one *) |
119 (* replaces the official subgoal antiquotation with one *) |