42 ML_Lex.read "val _ = NONE : (" @ ML_Lex.read_source false src @ ML_Lex.read ") option" |
42 ML_Lex.read "val _ = NONE : (" @ ML_Lex.read_source false src @ ML_Lex.read ") option" |
43 |
43 |
44 (* eval function *) |
44 (* eval function *) |
45 fun eval_fn ctxt prep exp = |
45 fun eval_fn ctxt prep exp = |
46 ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of exp) (prep exp) |
46 ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of exp) (prep exp) |
|
47 |
|
48 (* Evalate expression and convert result to a string *) |
|
49 fun eval_response ctxt exp = |
|
50 let |
|
51 fun compute exp = |
|
52 let |
|
53 val input = ML_Lex.read "(let val r = " @ ML_Lex.read_source false exp @ |
|
54 ML_Lex.read " in (raise ERROR (@{make_string} r); ()) end )" |
|
55 val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of exp) input |
|
56 in "" |
|
57 end |
|
58 in |
|
59 (compute exp |
|
60 handle ERROR s => s) |
|
61 end |
47 |
62 |
48 (* checks and prints a possibly open expressions, no index *) |
63 (* checks and prints a possibly open expressions, no index *) |
49 |
64 |
50 fun output_ml ctxt (src, (vs, stru)) = |
65 fun output_ml ctxt (src, (vs, stru)) = |
51 (eval_fn ctxt (ml_val vs stru) src; |
66 (eval_fn ctxt (ml_val vs stru) src; |
53 |
68 |
54 val parser_ml = Scan.lift (Args.text_input -- |
69 val parser_ml = Scan.lift (Args.text_input -- |
55 (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] -- |
70 (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] -- |
56 Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name))) |
71 Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name))) |
57 |
72 |
|
73 fun output_ml_response ctxt src = |
|
74 let |
|
75 val res = eval_response ctxt src |
|
76 in |
|
77 OutputTutorial.output ctxt ([Input.source_content src] @ [Library.prefix_lines "> " res]) |
|
78 end |
|
79 |
58 |
80 |
59 (* checks and prints a single ML-item and produces an index entry *) |
81 (* checks and prints a single ML-item and produces an index entry *) |
60 fun output_ml_ind ctxt (txt, stru) = |
82 fun output_ml_ind ctxt (src, stru) = |
61 (eval_fn ctxt (ml_val [] stru) (Input.string txt); |
83 let |
|
84 val txt = Input.source_content src |
|
85 in |
|
86 (eval_fn ctxt (ml_val [] stru) src; |
62 case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of |
87 case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of |
63 (NONE, _, "") => output_indexed ctxt {main = Code txt, minor = NoString} (split_lines txt) |
88 (NONE, _, "") => output_indexed ctxt {main = Code txt, minor = NoString} (split_lines txt) |
64 | (NONE, bn, qn) => output_indexed ctxt {main = Code bn, minor = Struct qn} (split_lines txt) |
89 | (NONE, bn, qn) => output_indexed ctxt {main = Code bn, minor = Struct qn} (split_lines txt) |
65 | (SOME st, _, _) => output_indexed ctxt {main = Code txt, minor = Struct st} (split_lines txt)) |
90 | (SOME st, _, _) => output_indexed ctxt {main = Code txt, minor = Struct st} (split_lines txt)) |
66 |
91 end |
67 val parser_ml_ind = Scan.lift (Args.name -- |
92 |
|
93 val parser_ml_ind = Scan.lift (Args.text_input -- |
68 Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name)) |
94 Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name)) |
69 |
95 |
70 (* checks and prints structures *) |
96 (* checks and prints structures *) |
71 fun gen_output_struct outfn ctxt txt = |
97 fun gen_output_struct outfn ctxt src = |
72 (eval_fn ctxt ml_struct (Input.string txt); |
98 let |
|
99 val txt = Input.source_content src |
|
100 in |
|
101 (eval_fn ctxt ml_struct src; |
73 outfn {main = Code txt, minor = Plain "structure"} (split_lines txt)) |
102 outfn {main = Code txt, minor = Plain "structure"} (split_lines txt)) |
|
103 end |
74 |
104 |
75 fun output_struct ctxt = gen_output_struct (K (output ctxt)) ctxt |
105 fun output_struct ctxt = gen_output_struct (K (output ctxt)) ctxt |
76 fun output_struct_ind ctxt = gen_output_struct (output_indexed ctxt) ctxt |
106 fun output_struct_ind ctxt = gen_output_struct (output_indexed ctxt) ctxt |
77 |
107 |
78 (* prints functors; no checks *) |
108 (* prints functors; no checks *) |
79 fun gen_output_funct outfn txt = |
109 fun gen_output_funct outfn src = |
|
110 let |
|
111 val txt = Input.source_content src |
|
112 in |
80 (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt)) |
113 (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt)) |
|
114 end |
81 |
115 |
82 fun output_funct ctxt = gen_output_funct (K (output ctxt)) |
116 fun output_funct ctxt = gen_output_funct (K (output ctxt)) |
83 fun output_funct_ind ctxt = gen_output_funct (output_indexed ctxt) |
117 fun output_funct_ind ctxt = gen_output_funct (output_indexed ctxt) |
84 |
118 |
85 (* checks and prints types *) |
119 (* checks and prints types *) |
86 fun gen_output_type outfn ctxt txt = |
120 fun gen_output_type outfn ctxt src = |
87 (eval_fn ctxt ml_type (Input.string txt); |
121 let |
|
122 val txt = Input.source_content src |
|
123 in |
|
124 (eval_fn ctxt ml_type src; |
88 outfn {main = Code txt, minor = Plain "type"} (split_lines txt)) |
125 outfn {main = Code txt, minor = Plain "type"} (split_lines txt)) |
|
126 end |
89 |
127 |
90 fun output_type ctxt = gen_output_type (K (output ctxt)) ctxt |
128 fun output_type ctxt = gen_output_type (K (output ctxt)) ctxt |
91 fun output_type_ind ctxt = gen_output_type (output_indexed ctxt) ctxt |
129 fun output_type_ind ctxt = gen_output_type (output_indexed ctxt) ctxt |
92 |
130 |
93 val dots_pat = translate_string (fn "_" => "\<dots>" | s => s) |
131 val dots_pat = translate_string (fn "_" => "\<dots>" | s => s) |
107 (* checks the expressions, but does not check it against a result pattern *) |
145 (* checks the expressions, but does not check it against a result pattern *) |
108 fun ouput_response_fake_both ctxt (lhs, pat) = |
146 fun ouput_response_fake_both ctxt (lhs, pat) = |
109 (output ctxt ((split_lines (Input.source_content lhs)) @ |
147 (output ctxt ((split_lines (Input.source_content lhs)) @ |
110 (prefix_lines "> " (dots_pat (Input.source_content pat))))) |
148 (prefix_lines "> " (dots_pat (Input.source_content pat))))) |
111 |
149 |
112 val single_arg = Scan.lift (Args.name) |
150 val single_arg = Scan.lift (Args.text_input) |
113 val two_args = Scan.lift (Args.text_input -- Args.text_input) |
151 val two_args = Scan.lift (Args.text_input -- Args.text_input) |
114 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) |
152 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) |
115 |
153 |
116 val ml_setup = |
154 val ml_setup = |
117 Thy_Output.antiquotation_raw @{binding "ML"} parser_ml output_ml |
155 Thy_Output.antiquotation_raw @{binding "ML"} parser_ml output_ml |
|
156 #> Thy_Output.antiquotation_raw @{binding "ML_response"} single_arg output_ml_response |
118 #> Thy_Output.antiquotation_raw @{binding "ML_ind"} parser_ml_ind output_ml_ind |
157 #> Thy_Output.antiquotation_raw @{binding "ML_ind"} parser_ml_ind output_ml_ind |
119 #> Thy_Output.antiquotation_raw @{binding "ML_type"} single_arg output_type |
|
120 #> Thy_Output.antiquotation_raw @{binding "ML_type_ind"} single_arg output_type_ind |
158 #> Thy_Output.antiquotation_raw @{binding "ML_type_ind"} single_arg output_type_ind |
121 #> Thy_Output.antiquotation_raw @{binding "ML_struct"} single_arg output_struct |
159 #> Thy_Output.antiquotation_raw @{binding "ML_structure_ind"} single_arg output_struct_ind |
122 #> Thy_Output.antiquotation_raw @{binding "ML_struct_ind"} single_arg output_struct_ind |
160 #> Thy_Output.antiquotation_raw @{binding "ML_functor_ind"} single_arg output_funct_ind |
123 #> Thy_Output.antiquotation_raw @{binding "ML_funct"} single_arg output_funct |
161 #> Thy_Output.antiquotation_raw @{binding "ML_matchresult"} two_args output_response |
124 #> Thy_Output.antiquotation_raw @{binding "ML_funct_ind"} single_arg output_funct_ind |
162 #> Thy_Output.antiquotation_raw @{binding "ML_matchresult_fake"} two_args output_response_fake |
125 #> Thy_Output.antiquotation_raw @{binding "ML_response"} two_args output_response |
163 #> Thy_Output.antiquotation_raw @{binding "ML_matchresult_fake_both"} two_args ouput_response_fake_both |
126 #> Thy_Output.antiquotation_raw @{binding "ML_response_fake"} two_args output_response_fake |
|
127 #> Thy_Output.antiquotation_raw @{binding "ML_response_fake_both"} two_args ouput_response_fake_both |
|
128 |
164 |
129 (* checks whether a file exists in the Isabelle distribution *) |
165 (* checks whether a file exists in the Isabelle distribution *) |
130 fun href_link txt = |
166 fun href_link txt = |
131 let |
167 let |
132 val raw = I (* FIXME: Symbol.encode_raw *) |
168 val raw = I (* FIXME: Symbol.encode_raw *) |
133 val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/" |
169 val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/" |
134 in |
170 in |
135 implode [raw "\\href{", raw path, raw txt, raw "}{", get_word txt, raw "}"] |
171 implode [raw "\\href{", raw path, raw txt, raw "}{", get_word txt, raw "}"] |
136 end |
172 end |
137 |
173 |
138 fun check_file_exists _ txt = |
174 fun check_file_exists _ src = |
|
175 let |
|
176 val txt = Input.source_content src |
|
177 in |
139 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
178 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
140 then Latex.string (href_link txt) |
179 then Latex.string (href_link txt) |
141 else error (implode ["Source file ", quote txt, " does not exist."])) |
180 else error (implode ["Source file ", quote txt, " does not exist."])) |
|
181 end |
142 |
182 |
143 val ml_file_setup = Thy_Output.antiquotation_raw @{binding "ML_file"} single_arg check_file_exists |
183 val ml_file_setup = Thy_Output.antiquotation_raw @{binding "ML_file"} single_arg check_file_exists |
144 |
184 |
145 |
185 |
146 (* replaces the official subgoal antiquotation with one *) |
186 (* replaces the official subgoal antiquotation with one *) |