# Read a single token after skipping preceding whitespaces
	#
	# Returns an empty string when at `eof`
	protected fun read_token: String
	do
		while not eof and src[pos].is_whitespace and src[pos] != '\n' do
			pos += 1
		end

		var start = pos
		ignore_until_whitespace_or_comment
		var ending = pos
		var str = src.substring(start, ending-start)
		return str
	end