class interface TEXT_FILE_READ
   --
   -- Basic input facilities to read a named file on the disc.
   --
   -- Note: most features are common with STD_INPUT so you can test your
   --       program on the screen first and then, just changing of
   --       instance (STD_INPUT/TEXT_FILE_READ), doing the same in a file.
   --

creation
   make
      -- The new created object is not connected. (See also connect_to.)

      ensure
         not is_connected

   connect_to (new_path: STRING)
      --  Open text file for reading. The stream is positioned at the
      --  beginning of the file.

      require
         not is_connected;
         not new_path.is_empty

feature(s) from INPUT_STREAM
   -- State of the stream:

   is_connected: BOOLEAN
      -- Is this file connected to some file of the operating system?

      ensure
         definition: Result = (path /= Void)

   end_of_input: BOOLEAN
      -- Has end-of-input been reached ?
      -- True when the last character has been read.


feature(s) from INPUT_STREAM
   -- To read one character at a time:

   read_character
      -- Read a character and assign it to last_character.

      require
         is_connected;
         not end_of_input
      ensure
         not push_back_flag

   last_character: CHARACTER
      -- Last character read with read_character.


   push_back_flag: BOOLEAN
      -- True if 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
      -- Skip all separators (see is_separator of class CHARACTER) and
      -- make the first non-separator available in last_character. This
      -- non-separator character is pushed back into the stream (see
      -- unread_character) to be available one more time (the next
      -- read_character will consider this non-separator). When
      -- end_of_input occurs, this process is automatically stopped.

      require
         is_connected;
         not end_of_input

   skip_separators_using (separators: STRING)
      -- Same job as skip_separators using the separators set.

      require
         is_connected;
         separators /= Void;
         not end_of_input

   skip_remainder_of_line
      -- Skip all the remainder of the line including the end of
      -- line character itself.


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
         is_connected;
         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
         is_connected;
         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
         is_connected;
         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 the unique common buffer to get for example the result
      -- computed by read_line, read_word, newline, etc. This is a
      -- once function (the same common buffer is used for all streams).


   read_line
      -- Read a complete line ended by '%N' or end_of_input. Make the
      -- result available in last_string common buffer. The end of line
      -- character (usually '%N') is not added in the last_string buffer.

      require
         is_connected;
         not end_of_input

   read_word
      -- Read a word using is_separator of class CHARACTER. Result is
      -- available in the last_string common buffer. 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
         is_connected;
         not end_of_input

   newline
      -- Consume input until newline ('%N') is found. Corresponding
      -- STRING is stored in last_string common buffer.


   reach_and_skip (keyword: STRING)
      -- Try to skip enough characters in order to reach the keyword
      -- which is skipped too. If the keyword is not in the remainder of
      -- this stream, the process is stopped as soon  as end_of_input
      -- occurs. As for skip_separators the following character of the
      -- keyword is available in last_character and not yet read.

      require
         not keyword.is_empty
      ensure
         not end_of_input implies last_string.is_equal(keyword)

feature(s) from INPUT_STREAM
   -- Other features:

   read_line_in (str: STRING)
      -- Same jobs as read_line but storage is directly done in buffer.
      --

      require
         is_connected;
         not end_of_input;
         str /= Void

   read_word_using (separators: STRING)
      -- Same jobs as read_word using separators.

      require
         is_connected;
         not end_of_input;
         separators /= Void

   read_tail_in (str: STRING)
      -- Read all remaining character of the file in str.

      require
         is_connected;
         str /= Void
      ensure
         end_of_input

feature(s) from FILE   connect_to (new_path: STRING)
      --  Open text file for reading. The stream is positioned at the
      --  beginning of the file.

      require
         not is_connected;
         not new_path.is_empty

   disconnect
      -- Disconnect from any file.

      require
         is_connected
      ensure
         not is_connected

feature(s) from TEXT_FILE_READ   path: STRING
      -- Not Void when connected to the corresponding file on the disk.




end of TEXT_FILE_READ