equal
deleted
inserted
replaced
167 |
167 |
168 (* input *) |
168 (* input *) |
169 |
169 |
170 val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos))); |
170 val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos))); |
171 |
171 |
172 val input_explode = |
172 val {explode_token, ...} = ML_Env.operations opt_context (#environment flags); |
173 if ML_Env.is_standard (#read (ML_Env.parse_environment opt_context (#environment flags))) |
173 fun token_content tok = if ML_Lex.is_comment tok then NONE else SOME (`explode_token tok); |
174 then String.explode |
|
175 else maps (String.explode o Symbol.esc) o Symbol.explode; |
|
176 |
|
177 fun token_content tok = |
|
178 if ML_Lex.is_comment tok then NONE |
|
179 else SOME (input_explode (ML_Lex.check_content_of tok), tok); |
|
180 |
174 |
181 val input_buffer = |
175 val input_buffer = |
182 Unsynchronized.ref (map_filter token_content toks); |
176 Unsynchronized.ref (map_filter token_content toks); |
183 |
177 |
184 fun get () = |
178 fun get () = |