# Flush the specified buffer as a `characters` event.
	#
	# Do nothing if `buffer` is empty.
	private fun flush(buffer: Buffer) do
		if buffer.length > 0 then
			model.fire_characters(buffer.to_s)
			buffer.clear
		end
	end