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 -- Bothfeature(s) from F_TEXTFILE -- Mode set_textmode_standard -- Both and are separators, lonely are ignored set_textmode_dos -- and are separators, lonely are ignored set_textmode_unix -- is the only separator. both lonely and are -- ignored. 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