class interface STD_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/STD_FILE_READ), doing the same in a file.
   -- 

creation
   connect_to (new_path: STRING)
      require
         not is_connected;
         not new_path.empty

   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 (buffer: 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_FILE_READ
   path: STRING
      --  Not Void when connected to the corresponding file 
      --  on the disk.


feature(s) from STD_FILE_READ
   make

   connect_to (new_path: STRING)
      require
         not is_connected;
         not new_path.empty

feature(s) from STD_FILE_READ
   disconnect
      require
         is_connected


end of STD_FILE_READ