- # Unread some characters.
- # Unread characters are stored in the pushback buffer.
- private fun push_back(accept_length: Int)
- do
- var length = _text.length
- var i = length - 1
- while i >= accept_length do
- _eof = false
- _stream_pos = _stream_pos + 1
- _stream_buf[_stream_pos] = _text[i]
- i = i - 1
- end
- end