class interface STD_FILE_READ_WRITE
   -- 
   --  Originally written by Emmanuel CECCHET --
   -- 

creation
   connect_to (new_path: STRING)

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

   is_connected: BOOLEAN

   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.


   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 OUTPUT_STREAM
   --  To write one character at a time :

   put_character (c: CHARACTER)
      require
         is_connected

feature(s) from OUTPUT_STREAM
   put_string (s: STRING)
      --  Output s to current output device.

      require
         is_connected;
         s /= Void

feature(s) from OUTPUT_STREAM
   --  To write a number :

   put_integer (i: INTEGER)
      --  Output i to current output device.

      require
         is_connected

   put_integer_format (i, s: INTEGER)
      --  Output i to current output device using at most
      --  s character.

      require
         is_connected

   put_real (r: REAL)
      --  Output r to current output device.

      require
         is_connected

   put_real_format (r: REAL; f: INTEGER)
      --  Output r with only f digit for the fractionnal part.
      --  Examples: 
      --     put_real(3.519,2) print "3.51".

      require
         is_connected;
         f >= 0

   put_double (d: DOUBLE)
      --  Output d to current output device.

      require
         is_connected

   put_double_format (d: DOUBLE; f: INTEGER)
      --  Output d with only f digit for the fractionnal part.
      --  Examples: 
      --     put_double(3.519,2) print "3.51". 

      require
         is_connected;
         f >= 0

feature(s) from OUTPUT_STREAM
   --  Other features :   

   put_boolean (b: BOOLEAN)
      --  Output b to current output device according
      --  to the Eiffel format.

      require
         is_connected

   put_pointer (p: POINTER)
      --  Output a viewable version of p.

      require
         is_connected

   put_new_line
      --  Output a newline character.

      require
         is_connected

   put_spaces (nb: INTEGER)
      --  Output nb spaces character.

      require
         nb >= 0

   append_file (file_name: STRING)
      require
         is_connected;
         file_exists(file_name)

   flush

feature(s) from STD_FILE_READ_WRITE
   path: STRING

feature(s) from STD_FILE_READ_WRITE
   connect_to (new_path: STRING)

feature(s) from STD_FILE_READ_WRITE
   disconnect
      require
         is_connected


end of STD_FILE_READ_WRITE