# Read the next useful line from file-name arguments
	private fun read_next_line
	do
		while stdin.eof do
			open_next_stream
		end
		self.line = stdin.read_line
	end