# read_line();; Exception: End_of_file.
read_line();;
Exception: End_of_file.