class interface F_TEXTFILE

creation
   make
      --  Create textfile.


feature(s) from MEMORY
   --  Removal :

   dispose
      --  Close file handle.

      ensure
         done: handle = Invalid_handle_value

   full_collect
      --  Force a full collection cycle if garbage collection is
      --  enabled; do nothing otherwise.


feature(s) from F_STREAM
   --  Constant

   Byte_maximum: INTEGER

feature(s) from F_STREAM
   --  Access

   connect
      --  Open the file.

      ensure
         can_fail:  --  success implies is_alive

   imperative_connect
      --  Open the file and raise an exception if failed.

      ensure
         valid: is_alive

   disconnect
      --  Close the file 
      --  (REQUIRED in order to flush temporary buffers).

      require
         valid: is_alive
      ensure
         done: not is_alive

feature(s) from F_STREAM
   --  Status

   is_alive: BOOLEAN
      --  Is the file stream open? (validity and openess is the same 
      --  for this kind of stream).


   has_data: BOOLEAN
      --  Is at least one byte waiting to be read?

      require
         valid: is_alive

   has_error: BOOLEAN
      --  Has the stream got errors?


   is_readable: BOOLEAN
      --  Is the stream readable?


   is_writable: BOOLEAN
      --  Is the stream writable?


feature(s) from F_STREAM
   --  Read/write

   last_byte: INTEGER
      --  Last byte read.

      ensure
         byte_size: Result >= 0 and then Result <= Byte_maximum

   read_byte
      --  Read one byte and update last byte.

      require
         valid: is_alive;
         readable: is_readable;
         available: has_data

   write_byte (b: INTEGER)
      --  Write a byte.

      require
         valid: is_alive;
         writable: is_writable;
         byte_size: b >= 0 and then b <= Byte_maximum

feature(s) from F_FILE
   --  Assertions

   is_valid_name (str: STRING): BOOLEAN
      --  Is the string a valid (Win32) file name?

      require
         valid: str /= Void

feature(s) from F_FILE
   --  Access mode

   set_name (str: STRING)
      --  Set the file name.

      require
         closed: not is_alive;
         valid_string: str /= Void;
         valid_file_name: is_valid_name(str)

   set_mode_read
      --  Set mode to be read only (default).

      require
         closed: not is_alive

   reset_mode
      --  Set mode to be read only (default).

      require
         closed: not is_alive

   set_mode_write
      --  Set mode to write only.

      require
         closed: not is_alive

   set_mode_read_write
      --  Set mode to be read/write.

      require
         closed: not is_alive

   set_share_read
      --  Set sharing to read.

      require
         closed: not is_alive

   reset_share
      --  Set sharing mode to no sharing (default).

      require
         closed: not is_alive

   set_share_no
      --  Set sharing mode to no sharing (default).

      require
         closed: not is_alive

   reset_open
      --  Create new file or reset existing one.

      require
         closed: not is_alive; --  when is_writable
         relevant: 

   set_open_zero
      --  Create new file or reset existing one.

      require
         closed: not is_alive; --  when is_writable
         relevant: 

   set_open_new
      --  Create new file, fail if file exists.

      require
         closed: not is_alive; --  when is_writable
         relevant: 

   set_open_existing
      --  Open existing file only.

      require
         closed: not is_alive; --  when is_writable
         relevant: 

   set_open_replace
      --  Open existing file and truncate it, fail if there 
      --  is no existing file.

      require
         closed: not is_alive;
         writable: is_writable

   set_open_always
      --  Open existing file without changing it, or create 
      --  if no file exists.

      require
         closed: not is_alive; --  when is_writable
         relevant: 

feature(s) from F_FILE
   --  Access

   is_open: BOOLEAN
      --  Is the file stream open? (validity and openess is the same 
      --  for this kind of stream).


feature(s) from F_FILE
   --  Block

   write_block (memory: F_MEMORY)
      --  Write a memory block to disk.

      require
         alive: is_alive;
         writable: is_writable

   read_block (req_size: INTEGER)
      --  Read a fixed size block from stream.

      require
         size_ok: req_size > 0;
         alive: is_alive;
         readable: is_readable;
         waiting: has_data
      ensure
         block_of: not has_error implies last_block /= Void and then last_block.size = req_size

   last_block: F_MEMORY
      --  Last memory block read (new block for each read operation).


feature(s) from F_TEXTFILE
   --  Mode

   reset_textmode
      --  Both  and  are separators, lonely  are ignored


feature(s) from F_TEXTFILE
   --  Mode

   set_textmode_standard
      --  Both  and  are separators, lonely  are ignored


   set_textmode_dos
      --   is the only separator. both lonely  and  are 
      --  ignored.


   set_textmode_unix
      --   are separators.


   set_textmode_character (chr: CHARACTER)
      --  The above character is the sole separator.


feature(s) from F_TEXTFILE
   --  Simple character access

   last_character: CHARACTER
      --  Last character read.


   read_character
      --  Read a character.

      require
         readable: is_readable;
         valid: is_alive;
         data: has_data

   write_character (c: CHARACTER)
      --  Write a character.

      require
         writable: is_writable;
         valid: is_alive

feature(s) from F_TEXTFILE
   --  Read/write line

   last_string: STRING
      --  Last read string (fresh object for each read_string).


   read_string
      --  Read the string into last_string. Separator char(s) are not put at 
      --  the end of the string.

      require
         valid: is_alive;
         readable: is_readable;
         data: has_data

   write_string (ostr: STRING)
      --  Write a line to the file (a separator character is 
      --  automatically added).

      require
         valid_string: ostr /= Void;
         valid_file: is_alive;
         writable: is_writable

invariant
   valid_index: buffer_index <= buffer_max;
   valid_buffer: is_alive implies buffer /= Void;
   valid_separator: textmode_crlf or textmode_char; --  Character_bits = 8
   valid_char: 

end of F_TEXTFILE