class interface STD_INPUT -- -- To use the standard input file. As for UNIX, the default standard -- input is the keyboard. -- -- Notes : - the predefined std_input should be use to have only -- one instance of the class STD_INPUT. -- - to do reading or writing at the same time on the screen, -- see STD_INPUT_OUTPUT, -- - to handle cursor of the screen, see CURSES. -- creation make feature(s) from INPUT_STREAM -- State of the stream : is_connected: BOOLEAN -- True when the corresponding stream is connected -- to some physical input device. end_of_input: BOOLEAN -- Has end-of-input been reached ? -- True when the last character has been read. require is_connected feature(s) from INPUT_STREAM -- To read one character at a time : read_character -- Read a character and assign it to last_character. require not end_of_input ensure not push_back_flag last_character: CHARACTER -- Last character read with read_character. require is_connected push_back_flag: BOOLEAN -- True in one char is already pushed back. unread_character -- Un-read the last character read. -- require not push_back_flag ensure push_back_flag feature(s) from INPUT_STREAM -- Skipping separators : skip_separators -- Stop doing read_character as soon as end_of_file is reached -- or as soon as last_character is not is_separator. -- When first character is already not is_separator nothing -- is done. skip_separators_using (separators: STRING) -- Same job as skip_separators using separators. require separators /= Void feature(s) from INPUT_STREAM -- To read one number at a time : read_integer -- Read an integer according to the Eiffel syntax. -- Make result available in last_integer. -- Heading separators are automatically skipped using -- is_separator of class CHARACTER. -- Trailing separators are not skipped. require not end_of_input last_integer: INTEGER -- Last integer read using read_integer. read_real -- Read a REAL and make the result available in last_real -- and in last_double. -- The integral part is available in last_integer. require not end_of_input last_real: REAL -- Last real read with read_real. read_double -- Read a DOUBLE and make the result available in -- last_double. require not end_of_input last_double: DOUBLE -- Last double read with read_double. feature(s) from INPUT_STREAM -- To read one line or one word at a time : last_string: STRING -- Access to a unique STRING to get the result computed -- with read_line, read_word or newline. -- No new STRING is allocated. read_line -- Read a complete line ended by '%N' or end_of_input. -- Make the result available in last_string. -- Character '%N' is not added in last_string. -- -- NOTE: the result is available in last_string without any -- memory allocation. require not end_of_input read_word -- Read a word using is_separator of class CHARACTER. -- Result is available in last_string (no allocation -- of memory). -- Heading separators are automatically skipped. -- Trailing separators are not skipped (last_character is -- left on the first one). -- If end_of_input is encountered, Result can be the -- empty string. require not end_of_input newline -- Consume input until newline ('%N') is found. -- Corresponding STRING is stored in last_string. feature(s) from INPUT_STREAM -- Other features : read_line_in (str: STRING) -- Same jobs as read_line but storage is directly done in str. -- require not end_of_input read_word_using (separators: STRING) -- Same jobs as read_word using separators. require not end_of_input; separators /= Void read_tail_in (str: STRING) -- Read all remaining character of the file in str. require str /= Void ensure end_of_input feature(s) from STD_INPUT make end of STD_INPUT