indexing
description: "Files viewed as persistent sequences of ASCII characters"
class interface
PLAIN_TEXT_FILE
create
make (fn: STRING)
-- Create file object with fn as file name.
-- (from FILE)
require -- from FILE
string_exists: fn /= void;
string_not_empty: not fn.empty
ensure -- from FILE
file_named: name.is_equal (fn);
file_closed: is_closed
make_open_read (fn: STRING)
-- Create file object with fn as file name
-- and open file in read mode.
-- (from FILE)
require -- from FILE
string_exists: fn /= void;
string_not_empty: not fn.empty
ensure -- from FILE
exists: exists;
open_read: is_open_read
make_open_write (fn: STRING)
-- Create file object with fn as file name
-- and open file for writing;
-- create it if it does not exist.
-- (from FILE)
require -- from FILE
string_exists: fn /= void;
string_not_empty: not fn.empty
ensure -- from FILE
exists: exists;
open_write: is_open_write
make_open_append (fn: STRING)
-- Create file object with fn as file name
-- and open file in append-only mode.
-- (from FILE)
require -- from FILE
string_exists: fn /= void;
string_not_empty: not fn.empty
ensure -- from FILE
exists: exists;
open_append: is_open_append
make_open_read_write (fn: STRING)
-- Create file object with fn as file name
-- and open file for both reading and writing.
-- (from FILE)
require -- from FILE
string_exists: fn /= void;
string_not_empty: not fn.empty
ensure -- from FILE
exists: exists;
open_read: is_open_read;
open_write: is_open_write
make_create_read_write (fn: STRING)
-- Create file object with fn as file name
-- and open file for both reading and writing;
-- create it if it does not exist.
-- (from FILE)
require -- from FILE
string_exists: fn /= void;
string_not_empty: not fn.empty
ensure -- from FILE
exists: exists;
open_read: is_open_read;
open_write: is_open_write
make_open_read_append (fn: STRING)
-- Create file object with fn as file name
-- and open file for reading anywhere
-- but writing at the end only.
-- Create file if it does not exist.
-- (from FILE)
require -- from FILE
string_exists: fn /= void;
string_not_empty: not fn.empty
ensure -- from FILE
exists: exists;
open_read: is_open_read;
open_append: is_open_append
feature -- Initialization
make (fn: STRING)
-- Create file object with fn as file name.
-- (from FILE)
require -- from FILE
string_exists: fn /= void;
string_not_empty: not fn.empty
ensure -- from FILE
file_named: name.is_equal (fn);
file_closed: is_closed
make_create_read_write (fn: STRING)
-- Create file object with fn as file name
-- and open file for both reading and writing;
-- create it if it does not exist.
-- (from FILE)
require -- from FILE
string_exists: fn /= void;
string_not_empty: not fn.empty
ensure -- from FILE
exists: exists;
open_read: is_open_read;
open_write: is_open_write
make_open_append (fn: STRING)
-- Create file object with fn as file name
-- and open file in append-only mode.
-- (from FILE)
require -- from FILE
string_exists: fn /= void;
string_not_empty: not fn.empty
ensure -- from FILE
exists: exists;
open_append: is_open_append
make_open_read (fn: STRING)
-- Create file object with fn as file name
-- and open file in read mode.
-- (from FILE)
require -- from FILE
string_exists: fn /= void;
string_not_empty: not fn.empty
ensure -- from FILE
exists: exists;
open_read: is_open_read
make_open_read_append (fn: STRING)
-- Create file object with fn as file name
-- and open file for reading anywhere
-- but writing at the end only.
-- Create file if it does not exist.
-- (from FILE)
require -- from FILE
string_exists: fn /= void;
string_not_empty: not fn.empty
ensure -- from FILE
exists: exists;
open_read: is_open_read;
open_append: is_open_append
make_open_read_write (fn: STRING)
-- Create file object with fn as file name
-- and open file for both reading and writing.
-- (from FILE)
require -- from FILE
string_exists: fn /= void;
string_not_empty: not fn.empty
ensure -- from FILE
exists: exists;
open_read: is_open_read;
open_write: is_open_write
make_open_write (fn: STRING)
-- Create file object with fn as file name
-- and open file for writing;
-- create it if it does not exist.
-- (from FILE)
require -- from FILE
string_exists: fn /= void;
string_not_empty: not fn.empty
ensure -- from FILE
exists: exists;
open_write: is_open_write
feature -- Access
-- Time stamp of last access made to the inode.
-- (from FILE)
require -- from FILE
file_exists: exists
-- Time stamp (time of last modification)
-- (from FILE)
require -- from FILE
file_exists: exists
descriptor: INTEGER
-- File descriptor as used by the operating system.
-- (from FILE)
require -- from IO_MEDIUM
valid_handle: descriptor_available
require else -- from FILE
file_opened: not is_closed
descriptor_available: BOOLEAN
-- (from FILE)
file_info: UNIX_FILE_INFO
-- Collected information about the file.
-- (from FILE)
file_pointer: POINTER
-- File pointer as required in C
-- (from FILE)
group_id: INTEGER
-- Group identification of owner
-- (from FILE)
require -- from FILE
file_exists: exists
has (v: like item): BOOLEAN
-- Does structure include an occurrence of v?
-- (Reference or object equality,
-- based on object_comparison.)
-- (from LINEAR)
ensure -- from CONTAINER
not_found_in_empty: Result implies not empty
index_of (v: like item; i: INTEGER): INTEGER
-- Index of i-th occurrence of v.
-- 0 if none.
-- (Reference or object equality,
-- based on object_comparison.)
-- (from LINEAR)
require -- from LINEAR
positive_occurrences: i > 0
ensure -- from LINEAR
non_negative_result: Result >= 0
inode: INTEGER
-- I-node number
-- (from FILE)
require -- from FILE
file_exists: exists
item: CHARACTER
-- Current item
-- (from FILE)
require -- from ACTIVE
readable: readable
require -- from TRAVERSABLE
not_off: not off
links: INTEGER
-- Number of links on file
-- (from FILE)
require -- from FILE
file_exists: exists
name: STRING
-- File name
-- (from FILE)
occurrences (v: CHARACTER): INTEGER
-- Number of times v appears.
-- (Reference or object equality,
-- based on object_comparison.)
-- (from LINEAR)
ensure -- from BAG
non_negative_occurrences: Result >= 0
owner_name: STRING
-- Name of owner
-- (from FILE)
require -- from FILE
file_exists: exists
position: INTEGER
-- Current cursor position.
-- (from FILE)
protection: INTEGER
-- Protection mode, in decimal value
-- (from FILE)
require -- from FILE
file_exists: exists
retrieved: ANY
-- Retrieved object structure
-- To access resulting object under correct type,
-- use assignment attempt.
-- Will raise an exception (code Retrieve_exception)
-- if content is not a stored Eiffel structure.
-- (from FILE)
require -- from IO_MEDIUM
exists: exists;
is_open_read: is_open_read;
support_storable: support_storable
ensure -- from IO_MEDIUM
result_exists: Result /= void
separator: CHARACTER
-- ASCII code of character following last word read
-- (from FILE)
user_id: INTEGER
-- User identification of owner
-- (from FILE)
require -- from FILE
file_exists: exists
feature -- Measurement
count: INTEGER
-- Size in bytes (0 if no associated physical file)
-- (from FILE)
feature -- Status report
access_exists: BOOLEAN
-- Does physical file exist?
-- (Uses real UID.)
-- (from FILE)
after: BOOLEAN
-- Is there no valid cursor position to the right of cursor position?
-- (from FILE)
before: BOOLEAN
-- Is there no valid cursor position to the left of cursor position?
-- (from FILE)
changeable_comparison_criterion: BOOLEAN
-- May object_comparison be changed?
-- (Answer: yes by default.)
-- (from CONTAINER)
empty: BOOLEAN
-- Is structure empty?
-- (from FINITE)
end_of_file: BOOLEAN
-- Has an EOF been detected?
-- (from FILE)
require -- from FILE
opened: not is_closed
exhausted: BOOLEAN
-- Has structure been completely explored?
-- (from LINEAR)
ensure -- from LINEAR
exhausted_when_off: off implies Result
exists: BOOLEAN
-- Does physical file exist?
-- (Uses effective UID.)
-- (from FILE)
extendible: BOOLEAN
-- May new items be added?
-- (from FILE)
file_prunable: BOOLEAN
-- May items be removed?
-- (from FILE)
file_readable: BOOLEAN
-- Is there a current item that may be read?
-- (from FILE)
file_writable: BOOLEAN
-- Is there a current item that may be modified?
-- (from FILE)
Full: BOOLEAN is false
-- Is structure filled to capacity?
-- (from FILE)
is_access_executable: BOOLEAN
-- Is file executable by real UID?
-- (from FILE)
require -- from FILE
file_exists: exists
is_access_owner: BOOLEAN
-- Is file owned by real UID?
-- (from FILE)
require -- from FILE
file_exists: exists
is_access_readable: BOOLEAN
-- Is file readable by real UID?
-- (from FILE)
require -- from FILE
file_exists: exists
is_access_writable: BOOLEAN
-- Is file writable by real UID?
-- (from FILE)
require -- from FILE
file_exists: exists
is_block: BOOLEAN
-- Is file a block special file?
-- (from FILE)
require -- from FILE
file_exists: exists
is_character: BOOLEAN
-- Is file a character special file?
-- (from FILE)
require -- from FILE
file_exists: exists
is_closed: BOOLEAN
-- Is file closed?
-- (from FILE)
is_creatable: BOOLEAN
-- Is file creatable in parent directory?
-- (Uses effective UID to check that parent is writable
-- and file does not exist.)
-- (from FILE)
is_device: BOOLEAN
-- Is file a device?
-- (from FILE)
require -- from FILE
file_exists: exists
is_directory: BOOLEAN
-- Is file a directory?
-- (from FILE)
require -- from FILE
file_exists: exists
is_executable: BOOLEAN
-- Is file executable?
-- (Checks execute permission for effective UID.)
-- (from FILE)
require -- from IO_MEDIUM
handle_exists: exists
is_fifo: BOOLEAN
-- Is file a named pipe?
-- (from FILE)
require -- from FILE
file_exists: exists
is_open_append: BOOLEAN
-- Is file open for appending?
-- (from FILE)
is_open_read: BOOLEAN
-- Is file open for reading?
-- (from FILE)
is_open_write: BOOLEAN
-- Is file open for writing?
-- (from FILE)
is_owner: BOOLEAN
-- Is file owned by effective UID?
-- (from FILE)
require -- from FILE
file_exists: exists
is_plain: BOOLEAN
-- Is file a plain file?
-- (from FILE)
require -- from FILE
file_exists: exists
is_plain_text: BOOLEAN
-- Is file reserved for text (character sequences)? (Yes)
is_readable: BOOLEAN
-- Is file readable?
-- (Checks permission for effective UID.)
-- (from FILE)
require -- from IO_MEDIUM
handle_exists: exists
is_setgid: BOOLEAN
-- Is file setgid?
-- (from FILE)
require -- from FILE
file_exists: exists
is_setuid: BOOLEAN
-- Is file setuid?
-- (from FILE)
require -- from FILE
file_exists: exists
is_socket: BOOLEAN
-- Is file a named socket?
-- (from FILE)
require -- from FILE
file_exists: exists
is_sticky: BOOLEAN
-- Is file sticky (for memory swaps)?
-- (from FILE)
require -- from FILE
file_exists: exists
is_symlink: BOOLEAN
-- Is file a symbolic link?
-- (from FILE)
require -- from FILE
file_exists: exists
is_writable: BOOLEAN
-- Is file writable?
-- (Checks write permission for effective UID.)
-- (from FILE)
require -- from IO_MEDIUM
handle_exists: exists
last_character: CHARACTER
-- Last character read by read_character
-- (from IO_MEDIUM)
last_double: DOUBLE
-- Last double read by read_double
-- (from IO_MEDIUM)
last_integer: INTEGER
-- Last integer read by read_integer
-- (from IO_MEDIUM)
last_real: REAL
-- Last real read by read_real
-- (from IO_MEDIUM)
last_string: STRING
-- Last string read
-- (from IO_MEDIUM)
object_comparison: BOOLEAN
-- Must search operations use equal rather than =
-- for comparing references? (Default: no, use =.)
-- (from CONTAINER)
off: BOOLEAN
-- Is there no item?
-- (from FILE)
readable: BOOLEAN
-- Is there a current item that may be read?
-- (from SEQUENCE)
require -- from IO_MEDIUM
handle_exists: exists
Support_storable: BOOLEAN is false
-- Can medium be used to store an Eiffel structure?
writable: BOOLEAN
-- Is there a current item that may be modified?
-- (from SEQUENCE)
feature -- Status setting
close
-- Close file.
-- (from FILE)
require -- from IO_MEDIUM
medium_is_open: not is_closed
ensure then -- from FILE
is_closed: is_closed
compare_objects
-- Ensure that future search operations will use equal
-- rather than = for comparing references.
-- (from CONTAINER)
require -- from CONTAINER
changeable_comparison_criterion
ensure -- from CONTAINER
object_comparison
compare_references
-- Ensure that future search operations will use =
-- rather than equal for comparing references.
-- (from CONTAINER)
require -- from CONTAINER
changeable_comparison_criterion
ensure -- from CONTAINER
reference_comparison: not object_comparison
create_read_write
-- Open file in read and write mode;
-- create it if it does not exist.
-- (from FILE)
require -- from FILE
is_closed: is_closed
ensure -- from FILE
exists: exists;
open_read: is_open_read;
open_write: is_open_write
fd_open_append (fd: INTEGER)
-- Open file of descriptor fd in append mode.
-- (from FILE)
ensure -- from FILE
exists: exists;
open_append: is_open_append
fd_open_read (fd: INTEGER)
-- Open file of descriptor fd in read-only mode.
-- (from FILE)
ensure -- from FILE
exists: exists;
open_read: is_open_read
fd_open_read_append (fd: INTEGER)
-- Open file of descriptor fd
-- in read and write-at-end mode.
-- (from FILE)
ensure -- from FILE
exists: exists;
open_read: is_open_read;
open_append: is_open_append
fd_open_read_write (fd: INTEGER)
-- Open file of descriptor fd in read-write mode.
-- (from FILE)
ensure -- from FILE
exists: exists;
open_read: is_open_read;
open_write: is_open_write
fd_open_write (fd: INTEGER)
-- Open file of descriptor fd in write mode.
-- (from FILE)
ensure -- from FILE
exists: exists;
open_write: is_open_write
open_append
-- Open file in append-only mode;
-- create it if it does not exist.
-- (from FILE)
require -- from FILE
is_closed: is_closed
ensure -- from FILE
exists: exists;
open_append: is_open_append
open_read
-- Open file in read-only mode.
-- (from FILE)
require -- from FILE
is_closed: is_closed
ensure -- from FILE
exists: exists;
open_read: is_open_read
open_read_append
-- Open file in read and write-at-end mode;
-- create it if it does not exist.
-- (from FILE)
require -- from FILE
is_closed: is_closed
ensure -- from FILE
exists: exists;
open_read: is_open_read;
open_append: is_open_append
open_read_write
-- Open file in read and write mode.
-- (from FILE)
require -- from FILE
is_closed: is_closed
ensure -- from FILE
exists: exists;
open_read: is_open_read;
open_write: is_open_write
open_write
-- Open file in write-only mode;
-- create it if it does not exist.
-- (from FILE)
ensure -- from FILE
exists: exists;
open_write: is_open_write
recreate_read_write (fname: STRING)
-- Reopen in read-write mode with file of name fname;
-- create file if it does not exist.
-- (from FILE)
require -- from FILE
is_open: not is_closed;
valid_name: fname /= void
ensure -- from FILE
exists: exists;
open_read: is_open_read;
open_write: is_open_write
reopen_append (fname: STRING)
-- Reopen in append mode with file of name fname;
-- create file if it does not exist.
-- (from FILE)
require -- from FILE
is_open: not is_closed;
valid_name: fname /= void
ensure -- from FILE
exists: exists;
open_append: is_open_append
reopen_read (fname: STRING)
-- Reopen in read-only mode with file of name fname;
-- create file if it does not exist.
-- (from FILE)
require -- from FILE
is_open: not is_closed;
valid_name: fname /= void
ensure -- from FILE
exists: exists;
open_read: is_open_read
reopen_read_append (fname: STRING)
-- Reopen in read and write-at-end mode with file
-- of name fname; create file if it does not exist.
-- (from FILE)
require -- from FILE
is_open: not is_closed;
valid_name: fname /= void
ensure -- from FILE
exists: exists;
open_read: is_open_read;
open_append: is_open_append
reopen_read_write (fname: STRING)
-- Reopen in read-write mode with file of name fname.
-- (from FILE)
require -- from FILE
is_open: not is_closed;
valid_name: fname /= void
ensure -- from FILE
exists: exists;
open_read: is_open_read;
open_write: is_open_write
reopen_write (fname: STRING)
-- Reopen in write-only mode with file of name fname;
-- create file if it does not exist.
-- (from FILE)
require -- from FILE
is_open: not is_closed;
valid_name: fname /= void
ensure -- from FILE
exists: exists;
open_write: is_open_write
feature -- Cursor movement
back
-- Go back one position.
-- (from FILE)
require -- from BILINEAR
not_before: not before
ensure then -- from BILINEAR
moved_back: position = old position - 1
finish
-- Go to last position.
-- (from FILE)
require -- LINEAR
precursor: True
require else -- from FILE
file_opened: not is_closed
forth
-- Go to next position.
-- (from FILE)
require -- from LINEAR
not_after: not after
require else -- from FILE
file_opened: not is_closed
go (abs_position: INTEGER)
-- Go to the absolute position.
-- (New position may be beyond physical length.)
-- (from FILE)
require -- from FILE
file_opened: not is_closed;
non_negative_argument: abs_position >= 0
move (offset: INTEGER)
-- Advance by offset from current location.
-- (from FILE)
require -- from FILE
file_opened: not is_closed
next_line
-- Move to next input line.
-- (from FILE)
require -- from FILE
is_readable: file_readable
recede (abs_position: INTEGER)
-- Go to the absolute position backwards,
-- starting from end of file.
-- (from FILE)
require -- from FILE
file_opened: not is_closed;
non_negative_argument: abs_position >= 0
search (v: like item)
-- Move to first position (at or after current
-- position) where item and v are equal.
-- If structure does not include v ensure that
-- exhausted will be true.
-- (Reference or object equality,
-- based on object_comparison.)
-- (from BILINEAR)
ensure -- from LINEAR
object_found: (not exhausted and object_comparison) implies equal (v, item);
item_found: (not exhausted and not object_comparison) implies v = item
start
-- Go to first position.
-- (from FILE)
require -- TRAVERSABLE
precursor: True
require else -- from FILE
file_opened: not is_closed
feature -- Element change
add_permission (who, what: STRING)
-- Add read, write, execute or setuid permission
-- for who ('u', 'g' or 'o') to what.
-- (from FILE)
require -- from FILE
who_is_not_void: who /= void;
what_is_not_void: what /= void;
file_descriptor_exists: exists
append (f: like Current)
-- Append a copy of the contents of f.
-- (from FILE)
require -- from SEQUENCE
argument_not_void: s /= void
require else -- from FILE
target_is_closed: is_closed;
source_is_closed: f.is_closed
ensure -- from SEQUENCE
new_count: count >= old count
ensure then -- from FILE
new_count: count = old count + f.count;
files_closed: f.is_closed and is_closed
basic_store (object: ANY)
-- Produce an external representation of the
-- entire object structure reachable from object.
-- Retrievable within current system only.
-- (from FILE)
require -- from IO_MEDIUM
object_not_void: object /= void;
exists: exists;
is_open_write: is_open_write;
support_storable: support_storable
-- Time stamp of last change.
-- (from FILE)
require -- from FILE
file_exists: exists
change_group (new_group_id: INTEGER)
-- Change group of file to new_group_id found in
-- system password file.
-- (from FILE)
require -- from FILE
file_exists: exists
change_mode (mask: INTEGER)
-- Replace mode by mask.
-- (from FILE)
require -- from FILE
file_exists: exists
change_name (new_name: STRING)
-- Change file name to new_name
-- (from FILE)
require -- from FILE
not_new_name_void: new_name /= void;
file_exists: exists
ensure -- from FILE
name_changed: name.is_equal (new_name)
change_owner (new_owner_id: INTEGER)
-- Change owner of file to new_owner_id found in
-- system password file. On some systems this
-- requires super-user privileges.
-- (from FILE)
require -- from FILE
file_exists: exists
extend (v: CHARACTER)
-- Include v at end.
-- (from FILE)
require -- from COLLECTION
extendible: extendible
ensure -- from COLLECTION
item_inserted: has (v)
ensure then -- from BAG
one_more_occurrence: occurrences (v) = old (occurrences (v)) + 1
fill (other: CONTAINER [CHARACTER])
-- Fill with as many items of other as possible.
-- The representations of other and current structure
-- need not be the same.
-- (from COLLECTION)
require -- from COLLECTION
other_not_void: other /= void;
extendible
flush
-- Flush buffered data to disk.
-- Note that there is no guarantee that the operating
-- system will physically write the data to the disk.
-- At least it will end up in the buffer cache,
-- making the data visible to other processes.
-- (from FILE)
require -- from FILE
is_open: not is_closed
force (v: like item)
-- Add v to end.
-- (from SEQUENCE)
require -- from SEQUENCE
extendible: extendible
ensure then -- from SEQUENCE
new_count: count = old count + 1;
item_inserted: has (v)
general_store (object: ANY)
-- Produce an external representation of the
-- entire object structure reachable from object.
-- Retrievable from other systems for same platform
-- (machine architecture).
-- (from FILE)
require -- from IO_MEDIUM
object_not_void: object /= void;
exists: exists;
is_open_write: is_open_write;
support_storable: support_storable
independent_store (object: ANY)
-- Produce an external representation of the
-- entire object structure reachable from object.
-- Retrievable from other systems for the same or other
-- platform (machine architecture).
-- (from FILE)
require -- from IO_MEDIUM
object_not_void: object /= void;
exists: exists;
is_open_write: is_open_write;
support_storable: support_storable
link (fn: STRING)
-- Link current file to fn.
-- fn must not already exist.
-- (from FILE)
require -- from FILE
file_exists: exists
new_line
-- Write a new line character at current position.
-- Was declared in FILE as synonym of put_new_line and new_line.
-- (from FILE)
require -- from IO_MEDIUM
extendible: extendible
put (v: like item)
-- Add v to end.
-- (from SEQUENCE)
require -- from COLLECTION
extendible: extendible
ensure -- from COLLECTION
item_inserted: has (v)
ensure then -- from SEQUENCE
new_count: count = old count + 1
put_character (c: CHARACTER)
-- Write c at current position.
-- Was declared in FILE as synonym of put_character and putchar.
-- (from FILE)
require -- from IO_MEDIUM
extendible: extendible
put_new_line
-- Write a new line character at current position.
-- Was declared in FILE as synonym of put_new_line and new_line.
-- (from FILE)
require -- from IO_MEDIUM
extendible: extendible
put_string (s: STRING)
-- Write s at current position.
-- Was declared in FILE as synonym of put_string and putstring.
-- (from FILE)
require -- from IO_MEDIUM
extendible: extendible;
non_void: s /= void
putchar (c: CHARACTER)
-- Write c at current position.
-- Was declared in FILE as synonym of put_character and putchar.
-- (from FILE)
require -- from IO_MEDIUM
extendible: extendible
putstring (s: STRING)
-- Write s at current position.
-- Was declared in FILE as synonym of put_string and putstring.
-- (from FILE)
require -- from IO_MEDIUM
extendible: extendible;
non_void: s /= void
remove_permission (who, what: STRING)
-- Remove read, write, execute or setuid permission
-- for who ('u', 'g' or 'o') to what.
-- (from FILE)
require -- from FILE
who_is_not_void: who /= void;
what_is_not_void: what /= void;
file_descriptor_exists: exists
set_access (time: INTEGER)
-- Stamp with time (access only).
-- (from FILE)
require -- from FILE
file_exists: exists
ensure -- from FILE
date_unchanged: date = old date
-- Stamp with time (modification time only).
-- (from FILE)
require -- from FILE
file_exists: exists
ensure -- from FILE
date_updated: date = time
stamp (time: INTEGER)
-- Stamp with time (for both access and modification).
-- (from FILE)
require -- from FILE
file_exists: exists
ensure -- from FILE
touch
-- Update time stamp (for both access and modification).
-- (from FILE)
require -- from FILE
file_exists: exists
ensure -- from FILE
feature -- Removal
delete
-- Remove link with physical file.
-- File does not physically disappear from the disk
-- until no more processes reference it.
-- I/O operations on it are still possible.
-- A directory must be empty to be deleted.
-- (from FILE)
require -- from FILE
exists: exists
dispose
-- Ensure this medium is closed when garbage collected.
-- (from IO_MEDIUM)
prune_all (v: like item)
-- Remove all occurrences of v; go off.
-- (from SEQUENCE)
require -- from COLLECTION
prunable
ensure -- from COLLECTION
no_more_occurrences: not has (v)
reset (fn: STRING)
-- Change file name to fn and reset
-- file descriptor and all information.
-- (from FILE)
require -- from FILE
valid_file_name: fn /= void
ensure -- from FILE
file_renamed: name = fn;
file_closed: is_closed
wipe_out
-- Remove all items.
-- (from FILE)
require -- from COLLECTION
prunable
require else -- from FILE
is_closed: is_closed
ensure -- from COLLECTION
wiped_out: empty
feature -- Conversion
linear_representation: LINEAR [CHARACTER]
-- Representation as a linear structure
-- (from LINEAR)
feature -- Output
put_boolean (b: BOOLEAN)
-- Write ASCII value of b at current position.
-- Was declared in PLAIN_TEXT_FILE as synonym of put_boolean and putbool.
require -- from IO_MEDIUM
extendible: extendible
put_double (d: DOUBLE)
-- Write ASCII value d at current position.
-- Was declared in PLAIN_TEXT_FILE as synonym of put_double and putdouble.
require -- from IO_MEDIUM
extendible: extendible
put_integer (i: INTEGER)
-- Write ASCII value of i at current position.
-- Was declared in PLAIN_TEXT_FILE as synonym of put_integer and putint.
require -- from IO_MEDIUM
extendible: extendible
put_real (r: REAL)
-- Write ASCII value of r at current position.
-- Was declared in PLAIN_TEXT_FILE as synonym of put_real and putreal.
require -- from IO_MEDIUM
extendible: extendible
putbool (b: BOOLEAN)
-- Write ASCII value of b at current position.
-- Was declared in PLAIN_TEXT_FILE as synonym of put_boolean and putbool.
require -- from IO_MEDIUM
extendible: extendible
putdouble (d: DOUBLE)
-- Write ASCII value d at current position.
-- Was declared in PLAIN_TEXT_FILE as synonym of put_double and putdouble.
require -- from IO_MEDIUM
extendible: extendible
putint (i: INTEGER)
-- Write ASCII value of i at current position.
-- Was declared in PLAIN_TEXT_FILE as synonym of put_integer and putint.
require -- from IO_MEDIUM
extendible: extendible
putreal (r: REAL)
-- Write ASCII value of r at current position.
-- Was declared in PLAIN_TEXT_FILE as synonym of put_real and putreal.
require -- from IO_MEDIUM
extendible: extendible
feature -- Input
read_character
-- Read a new character.
-- Make result available in last_character.
-- Was declared in FILE as synonym of read_character and readchar.
-- (from FILE)
require -- from IO_MEDIUM
is_readable: readable
require else -- from FILE
is_readable: file_readable
read_double
-- Read the ASCII representation of a new double
-- from file. Make result available in last_double.
-- Was declared in PLAIN_TEXT_FILE as synonym of read_double and readdouble.
require -- from IO_MEDIUM
is_readable: readable
require else -- from FILE
is_readable: file_readable
read_integer
-- Read the ASCII representation of a new integer
-- from file. Make result available in last_integer.
-- Was declared in PLAIN_TEXT_FILE as synonym of read_integer and readint.
require -- from IO_MEDIUM
is_readable: readable
require else -- from FILE
is_readable: file_readable
read_line
-- Read a string until new line or end of file.
-- Make result available in last_string.
-- New line will be consumed but not part of last_string.
-- Was declared in FILE as synonym of read_line and readline.
-- (from FILE)
require -- from IO_MEDIUM
is_readable: readable
require else -- from FILE
is_readable: file_readable
read_real
-- Read the ASCII representation of a new real
-- from file. Make result available in last_real.
-- Was declared in PLAIN_TEXT_FILE as synonym of read_real and readreal.
require -- from IO_MEDIUM
is_readable: readable
require else -- from FILE
is_readable: file_readable
read_stream (nb_char: INTEGER)
-- Read a string of at most nb_char bound characters
-- or until end of file.
-- Make result available in last_string.
-- Was declared in FILE as synonym of read_stream and readstream.
-- (from FILE)
require -- from IO_MEDIUM
is_readable: readable
require else -- from FILE
is_readable: file_readable
read_word
-- Read a string, excluding white space and stripping
-- leading white space.
-- Make result available in last_string.
-- White space characters are: blank, new_line, tab,
-- vertical tab, formfeed, end of file.
-- Was declared in FILE as synonym of read_word and readword.
-- (from FILE)
require -- from FILE
is_readable: file_readable
readchar
-- Read a new character.
-- Make result available in last_character.
-- Was declared in FILE as synonym of read_character and readchar.
-- (from FILE)
require -- from IO_MEDIUM
is_readable: readable
require else -- from FILE
is_readable: file_readable
readdouble
-- Read the ASCII representation of a new double
-- from file. Make result available in last_double.
-- Was declared in PLAIN_TEXT_FILE as synonym of read_double and readdouble.
require -- from IO_MEDIUM
is_readable: readable
require else -- from FILE
is_readable: file_readable
readint
-- Read the ASCII representation of a new integer
-- from file. Make result available in last_integer.
-- Was declared in PLAIN_TEXT_FILE as synonym of read_integer and readint.
require -- from IO_MEDIUM
is_readable: readable
require else -- from FILE
is_readable: file_readable
readline
-- Read a string until new line or end of file.
-- Make result available in last_string.
-- New line will be consumed but not part of last_string.
-- Was declared in FILE as synonym of read_line and readline.
-- (from FILE)
require -- from IO_MEDIUM
is_readable: readable
require else -- from FILE
is_readable: file_readable
readreal
-- Read the ASCII representation of a new real
-- from file. Make result available in last_real.
-- Was declared in PLAIN_TEXT_FILE as synonym of read_real and readreal.
require -- from IO_MEDIUM
is_readable: readable
require else -- from FILE
is_readable: file_readable
readstream (nb_char: INTEGER)
-- Read a string of at most nb_char bound characters
-- or until end of file.
-- Make result available in last_string.
-- Was declared in FILE as synonym of read_stream and readstream.
-- (from FILE)
require -- from IO_MEDIUM
is_readable: readable
require else -- from FILE
is_readable: file_readable
readword
-- Read a string, excluding white space and stripping
-- leading white space.
-- Make result available in last_string.
-- White space characters are: blank, new_line, tab,
-- vertical tab, formfeed, end of file.
-- Was declared in FILE as synonym of read_word and readword.
-- (from FILE)
require -- from FILE
is_readable: file_readable
feature -- Obsolete
lastchar: CHARACTER
-- Last character read by read_character
-- (from IO_MEDIUM)
lastdouble: DOUBLE
-- Last double read by read_double
-- (from IO_MEDIUM)
lastint: INTEGER
-- Last integer read by read_integer
-- (from IO_MEDIUM)
lastreal: REAL
-- Last real read by read_real
-- (from IO_MEDIUM)
laststring: STRING
-- Last string read
-- (from IO_MEDIUM)
invariant
-- from GENERAL
reflexive_equality: standard_is_equal (Current);
reflexive_conformance: conforms_to (Current);
plain_text: is_plain_text;
-- from FILE
name_exists: name /= void;
name_not_empty: not name.empty;
-- from FINITE
empty_definition: empty = (count = 0);
non_negative_count: count >= 0;
-- from ACTIVE
writable_constraint: writable implies readable;
empty_constraint: empty implies (not readable) and (not writable);
-- from BILINEAR
not_both: not (after and before);
empty_property: empty implies (after or before);
before_constraint: before implies off;
-- from LINEAR
after_constraint: after implies off;
-- from TRAVERSABLE
empty_constraint: empty implies off;
end -- class PLAIN_TEXT_FILE