44 |
44 |
45 ML%linenosgray\<open>fun ml_val code_txt = (ml_enclose "val _ = " "" code_txt) |
45 ML%linenosgray\<open>fun ml_val code_txt = (ml_enclose "val _ = " "" code_txt) |
46 |
46 |
47 fun output_ml ctxt code_txt = |
47 fun output_ml ctxt code_txt = |
48 let |
48 let |
49 val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_val code_txt) |
49 val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags |
|
50 (Input.pos_of code_txt) (ml_val code_txt) |
50 in |
51 in |
51 Pretty.str (fst (Input.source_content code_txt)) |
52 Pretty.str (fst (Input.source_content code_txt)) |
52 end |
53 end |
53 |
54 |
54 val ml_checked_setup = Thy_Output.antiquotation_pretty_source @{binding "ML_checked"} (Scan.lift Args.text_input) output_ml\<close> |
55 val ml_checked_setup = Thy_Output.antiquotation_pretty_source |
|
56 @{binding "ML_checked"} (Scan.lift Args.text_input) output_ml\<close> |
55 |
57 |
56 setup \<open>ml_checked_setup\<close> |
58 setup \<open>ml_checked_setup\<close> |
57 |
59 |
58 |
60 |
59 text \<open> |
61 text \<open> |
78 |
80 |
79 Since we used the argument @{ML \<open>Position.none\<close>}, the compiler cannot give specific |
81 Since we used the argument @{ML \<open>Position.none\<close>}, the compiler cannot give specific |
80 information about the line number, in case an error is detected. We |
82 information about the line number, in case an error is detected. We |
81 can improve the code above slightly by writing |
83 can improve the code above slightly by writing |
82 \<close> |
84 \<close> |
83 (* FIXME: remove |
|
84 ML%linenosgray{*fun output_ml ctxt (code_txt, pos) = |
|
85 let |
|
86 val srcpos = {delimited = false, pos = pos, text = ml_val code_txt} |
|
87 in |
|
88 (ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos; |
|
89 code_txt |
|
90 |> space_explode "\n" |
|
91 |> map Pretty.str |
|
92 |> Pretty.list "" "" |
|
93 |> Document_Antiquotation.output ctxt |
|
94 |> Latex.string) |
|
95 end |
|
96 |
85 |
97 val ml_checked_setup2 = Thy_Output.antiquotation @{binding "ML_checked2"} |
|
98 (Scan.lift (Parse.position Args.name)) output_ml *} |
|
99 |
|
100 setup {* ml_checked_setup2 *} |
|
101 *) |
|
102 text \<open> |
86 text \<open> |
103 where in Lines 1 and 2 the positional information is properly treated. The |
87 where in Lines 1 and 2 the positional information is properly treated. The |
104 parser @{ML Parse.position} encodes the positional information in the |
88 parser @{ML Parse.position} encodes the positional information in the |
105 result. |
89 result. |
106 |
90 |
127 ellipses from it and replace them by @{text [quotes] "_"}. The following |
111 ellipses from it and replace them by @{text [quotes] "_"}. The following |
128 function will do this: |
112 function will do this: |
129 \<close> |
113 \<close> |
130 |
114 |
131 ML%linenosgray\<open>fun ml_pat pat code = |
115 ML%linenosgray\<open>fun ml_pat pat code = |
132 ML_Lex.read "val" @ ML_Lex.read_source pat @ ML_Lex.read " = " @ ML_Lex.read_source code\<close> |
116 ML_Lex.read "val" @ |
|
117 ML_Lex.read_source pat @ |
|
118 ML_Lex.read " = " @ |
|
119 ML_Lex.read_source code\<close> |
133 |
120 |
134 (* |
|
135 ML %grayML{*fun ml_pat code_txt pat = |
|
136 let val pat' = |
|
137 implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) |
|
138 in |
|
139 ml_enclose ("val " ^ pat' ^ " = ") "" code_txt |
|
140 end*} |
|
141 *) |
|
142 text \<open> |
121 text \<open> |
143 Next we add a response indicator to the result using: |
122 Next we add a response indicator to the result using: |
144 \<close> |
123 \<close> |
145 |
124 |
146 |
125 |
151 \<close> |
130 \<close> |
152 |
131 |
153 ML %linenosgray\<open> |
132 ML %linenosgray\<open> |
154 fun output_ml_resp ctxt (code_txt, pat) = |
133 fun output_ml_resp ctxt (code_txt, pat) = |
155 let |
134 let |
156 val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_pat pat code_txt) |
135 val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags |
|
136 (Input.pos_of code_txt) (ml_pat pat code_txt) |
157 val code = space_explode "\n" (fst (Input.source_content code_txt)) |
137 val code = space_explode "\n" (fst (Input.source_content code_txt)) |
158 val resp = add_resp (space_explode "\n" (fst (Input.source_content pat))) |
138 val resp = add_resp (space_explode "\n" (fst (Input.source_content pat))) |
159 in |
139 in |
160 Pretty.str (cat_lines (code @ resp)) |
140 Pretty.str (cat_lines (code @ resp)) |
161 end |
141 end |
162 |
142 |
163 val ml_response_setup = Thy_Output.antiquotation_pretty_source @{binding "ML_resp"} (Scan.lift (Args.text_input -- Args.text_input)) output_ml_resp |
143 val ml_response_setup = Thy_Output.antiquotation_pretty_source |
|
144 @{binding "ML_resp"} |
|
145 (Scan.lift (Args.text_input -- Args.text_input)) |
|
146 output_ml_resp |
164 |
147 |
165 \<close> |
148 \<close> |
166 |
149 |
167 (* |
|
168 ML %linenosgray{*fun output_ml_resp {context = ctxt, ...} ((code_txt, pat), pos) = |
|
169 (let |
|
170 val srcpos = {delimited = false, text = ml_pat (code_txt, pat), pos = pos} |
|
171 in |
|
172 ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos |
|
173 end; |
|
174 let |
|
175 val code_output = space_explode "\n" code_txt |
|
176 val resp_output = add_resp (space_explode "\n" pat) |
|
177 in |
|
178 Thy_Output.output ctxt (map Pretty.str (code_output @ resp_output)) |
|
179 end) |
|
180 |
|
181 |
|
182 val ml_resp_setup = Thy_Output.antiquotation @{binding "ML_resp"} |
|
183 (Scan.lift (Parse.position (Args.text_input -- Args.text_input))) |
|
184 output_ml_resp*} |
|
185 *) |
|
186 setup \<open>ml_response_setup\<close> |
150 setup \<open>ml_response_setup\<close> |
187 |
151 |
188 (* FIXME *) |
152 (* FIXME *) |
189 text \<open> |
153 text \<open> |
190 In comparison with \<open>ML_checked\<close>, we only changed the line about |
154 In comparison with \<open>ML_checked\<close>, we only changed the line about |