75 |
73 |
76 val location_props = |
74 val location_props = |
77 op ^ (YXML.output_markup (Markup.position |> Markup.properties |
75 op ^ (YXML.output_markup (Markup.position |> Markup.properties |
78 (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos)))); |
76 (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos)))); |
79 |
77 |
80 val input = toks |> maps (fn tok => |
78 val input_buffer = |
81 let |
79 Unsynchronized.ref (toks |> map |
82 val syms = Symbol.explode (ML_Lex.check_content_of tok); |
80 (`(maps (String.explode o Symbol.esc) o Symbol.explode o ML_Lex.check_content_of))); |
83 val (ps, _) = fold_map (fn s => fn p => (p, Position.advance s p)) syms |
|
84 (Position.reset_range (ML_Lex.pos_of tok)); |
|
85 in |
|
86 (ps ~~ syms) |> maps (fn (p, sym) => |
|
87 map (pair (offset_of p)) (String.explode (Symbol.esc sym))) |
|
88 end); |
|
89 |
81 |
90 val input_buffer = Unsynchronized.ref input; |
|
91 val line = Unsynchronized.ref (the_default 1 (Position.line_of pos)); |
|
92 |
|
93 fun get_offset () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i); |
|
94 fun get () = |
82 fun get () = |
95 (case ! input_buffer of |
83 (case ! input_buffer of |
96 [] => NONE |
84 (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c) |
97 | (_, c) :: rest => |
85 | ([], _) :: rest => (input_buffer := rest; SOME #" ") |
98 (input_buffer := rest; |
86 | [] => NONE); |
99 if c = #"\n" then line := ! line + 1 else (); |
87 |
100 SOME c)); |
88 fun get_pos () = |
|
89 (case ! input_buffer of |
|
90 (_ :: _, tok) :: _ => ML_Lex.pos_of tok |
|
91 | ([], tok) :: _ => ML_Lex.end_pos_of tok |
|
92 | [] => Position.none); |
101 |
93 |
102 |
94 |
103 (* output channels *) |
95 (* output channels *) |
104 |
96 |
105 val writeln_buffer = Unsynchronized.ref Buffer.empty; |
97 val writeln_buffer = Unsynchronized.ref Buffer.empty; |
176 |
168 |
177 val parameters = |
169 val parameters = |
178 [PolyML.Compiler.CPOutStream write, |
170 [PolyML.Compiler.CPOutStream write, |
179 PolyML.Compiler.CPNameSpace space, |
171 PolyML.Compiler.CPNameSpace space, |
180 PolyML.Compiler.CPErrorMessageProc message, |
172 PolyML.Compiler.CPErrorMessageProc message, |
181 PolyML.Compiler.CPLineNo (fn () => ! line), |
173 PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos), |
182 PolyML.Compiler.CPLineOffset get_offset, |
174 PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos), |
183 PolyML.Compiler.CPFileName location_props, |
175 PolyML.Compiler.CPFileName location_props, |
184 PolyML.Compiler.CPCompilerResultFun result_fun, |
176 PolyML.Compiler.CPCompilerResultFun result_fun, |
185 PolyML.Compiler.CPPrintInAlphabeticalOrder false]; |
177 PolyML.Compiler.CPPrintInAlphabeticalOrder false]; |
186 val _ = |
178 val _ = |
187 (while not (List.null (! input_buffer)) do |
179 (while not (List.null (! input_buffer)) do |