equal
deleted
inserted
replaced
89 |
89 |
90 val end_pos = |
90 val end_pos = |
91 if null toks then Position.none |
91 if null toks then Position.none |
92 else ML_Lex.end_pos_of (List.last toks); |
92 else ML_Lex.end_pos_of (List.last toks); |
93 |
93 |
94 val input_buffer = ref (input @ [(offset_of end_pos, #"\n")]); |
94 val input_buffer = Unsynchronized.ref (input @ [(offset_of end_pos, #"\n")]); |
95 val line = ref (the_default 1 (Position.line_of pos)); |
95 val line = Unsynchronized.ref (the_default 1 (Position.line_of pos)); |
96 |
96 |
97 fun get_offset () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i); |
97 fun get_offset () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i); |
98 fun get () = |
98 fun get () = |
99 (case ! input_buffer of |
99 (case ! input_buffer of |
100 [] => NONE |
100 [] => NONE |
104 SOME c)); |
104 SOME c)); |
105 |
105 |
106 |
106 |
107 (* output *) |
107 (* output *) |
108 |
108 |
109 val output_buffer = ref Buffer.empty; |
109 val output_buffer = Unsynchronized.ref Buffer.empty; |
110 fun output () = Buffer.content (! output_buffer); |
110 fun output () = Buffer.content (! output_buffer); |
111 fun put s = change output_buffer (Buffer.add s); |
111 fun put s = Unsynchronized.change output_buffer (Buffer.add s); |
112 |
112 |
113 fun put_message {message, hard, location, context = _} = |
113 fun put_message {message, hard, location, context = _} = |
114 (put ((if hard then "Error" else "Warning") ^ Position.str_of (position_of location) ^ ":\n"); |
114 (put ((if hard then "Error" else "Warning") ^ Position.str_of (position_of location) ^ ":\n"); |
115 put (Pretty.string_of (Pretty.from_ML (pretty_ml message)) ^ "\n")); |
115 put (Pretty.string_of (Pretty.from_ML (pretty_ml message)) ^ "\n")); |
116 |
116 |