Eiffel Media API
Overview Cluster Class Classes Index      Previous Next      Top Features

kernel.io

Class KL_UNIX_OUTPUT_FILE


Direct ancestors

KI_TEXT_OUTPUT_FILE, KL_BINARY_OUTPUT_FILE

Creation

Features

Invariants

indexing

description

Unix-like text output files containing extended ASCII %
%characters (8-bit code between 0 and 255)

library

Gobo Eiffel Kernel Library

copyright

Copyright (c) 2001, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2005/07/13 17:05:07 $

revision

$Revision: 1.10 $

class

KL_UNIX_OUTPUT_FILE

inherit

KI_TEXT_OUTPUT_FILE
KL_BINARY_OUTPUT_FILE
KI_BINARY_OUTPUT_FILE
KL_OUTPUT_FILE
RAW_FILE
FILE
UNBOUNDED
FINITE
BOX
CONTAINER
SEQUENCE
ACTIVE
BAG
COLLECTION
CONTAINER
BILINEAR
LINEAR
TRAVERSABLE
CONTAINER
LINEAR
TRAVERSABLE
CONTAINER
FINITE
BOX
CONTAINER
IO_MEDIUM
STRING_HANDLER

create

make (a_name: like name)

-- Create a new file named a_name.
-- (a_name should follow the pathname convention
-- of the underlying platform. For pathname conversion
-- use KI_FILE_SYSTEM.pathname_from_file_system.)

-- (From KI_FILE_SYSTEM_ENTRY)

require
a_name_not_void: a_name /= Void
ensure
name_set: name = a_name
is_closed: is_closed

feature -- Initialization

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
string_exists: fn /= Void
string_not_empty: not fn.is_empty
ensure
file_named: name = fn
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
string_exists: fn /= Void
string_not_empty: not fn.is_empty
ensure
file_named: name = fn
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
string_exists: fn /= Void
string_not_empty: not fn.is_empty
ensure
file_named: name = fn
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
string_exists: fn /= Void
string_not_empty: not fn.is_empty
ensure
file_named: name = fn
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
string_exists: fn /= Void
string_not_empty: not fn.is_empty
ensure
file_named: name = fn
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
string_exists: fn /= Void
string_not_empty: not fn.is_empty
ensure
file_named: name = fn
exists: exists
open_write: is_open_write
old_make (fn: STRING)

-- Create file object with fn as file name.

-- (From KL_FILE)

require
string_exists: fn /= Void
string_not_empty: not fn.is_empty
ensure
file_named: string_name.is_equal (fn)
file_closed: old_is_closed
reset (a_name: STRING)

-- Reuse current Eiffel object memory to
-- represent a new file system entry.
-- (a_name should follow the pathname convention
-- of the underlying platform. For pathname conversion
-- use KI_FILE_SYSTEM.pathname_from_file_system.)

-- (From KI_FILE_SYSTEM_ENTRY)

require
a_name_not_void: a_name /= Void
is_closed: is_closed
ensure
name_set: name = a_name
is_closed: is_closed

feature {NONE} -- Initialization

make (a_name: like name)

-- Create a new file named a_name.
-- (a_name should follow the pathname convention
-- of the underlying platform. For pathname conversion
-- use KI_FILE_SYSTEM.pathname_from_file_system.)

-- (From KI_FILE_SYSTEM_ENTRY)

require
a_name_not_void: a_name /= Void
ensure
name_set: name = a_name
is_closed: is_closed

feature -- Access

any_: KL_ANY_ROUTINES

-- Routines that ought to be in class ANY

-- (From KL_IMPORTED_ANY_ROUTINES)

ensure
any_routines_not_void: Result /= Void
string_: KL_STRING_ROUTINES

-- Routines that ought to be in class STRING

-- (From KL_IMPORTED_STRING_ROUTINES)

ensure
string_routines_not_void: Result /= Void
access_date: INTEGER

-- Time stamp of last access made to the inode.

-- (From FILE)

require
file_exists: exists
date: INTEGER

-- Time stamp (time of last modification)

-- (From KL_FILE)

require
file_exists: old_exists
descriptor: INTEGER

-- File descriptor as used by the operating system.

-- (From IO_MEDIUM)

require
valid_handle: handle_available
require else
file_opened: not is_closed
descriptor_available: BOOLEAN

-- (From IO_MEDIUM)

eol: STRING

-- Line separator

-- (From KI_TEXT_OUTPUT_STREAM)

ensure
eol_not_void: Result /= Void
eol_not_empty: Result.count > 0
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
file_exists: exists
has (v: like item): BOOLEAN

-- Does structure include an occurrence of v?
-- (Reference or object equality,
-- based on object_comparison.)

-- (From CONTAINER)

ensure
not_found_in_empty: Result implies not is_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
positive_occurrences: i > 0
ensure
non_negative_result: Result >= 0
inode: INTEGER

-- I-node number

-- (From KL_FILE)

require
file_exists: old_exists
item: CHARACTER

-- Current item

-- (From ACTIVE)

require
readable: readable
links: INTEGER

-- Number of links on file

-- (From FILE)

require
file_exists: exists
name: STRING

-- File name;
-- Note: If name is a UC_STRING or descendant, then
-- the bytes of its associated UTF unicode encoding will
-- be used.

-- (From KI_FILE_SYSTEM_ENTRY)

ensure
name_not_void: Result /= Void
occurrences (v: CHARACTER): INTEGER

-- Number of times v appears.
-- (Reference or object equality,
-- based on object_comparison.)

-- (From BAG)

ensure
non_negative_occurrences: Result >= 0
owner_name: STRING

-- Name of owner

-- (From FILE)

require
file_exists: exists
position: INTEGER

-- Current cursor position.

-- (From FILE)

protection: INTEGER

-- Protection mode, in decimal value

-- (From FILE)

require
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 IO_MEDIUM)

require
is_readable: readable
support_storable: support_storable
ensure
Result_exists: Result /= Void
separator: CHARACTER

-- ASCII code of character following last word read

-- (From FILE)

sequential_search (v: like item)

-- Move to first position (at or after current
-- position) where item and v are equal.
-- (Reference or object equality,
-- based on object_comparison.)
-- If no such position ensure that exhausted will be true.

-- (From LINEAR)

ensure
object_found: (not exhausted and object_comparison)implies equal (v, item)
item_found: (not exhausted and not object_comparison)implies v = item
time_stamp: INTEGER

-- Time stamp (number of seconds since 1 January 1970
-- at 00:00:00 UTC) of last modification to current file;
-- Return -1 if the time stamp was not available, if the
-- file did not exist for example, or if the time stamp
-- didn't fit into an INTEGER. (Use DT_DATE_TIME.make_from_epoch
-- to convert this time stamp to a human readable format.)

-- (From KI_FILE)

ensure
valid_values: Result = -1 or Result >= 0
user_id: INTEGER

-- User identification of owner

-- (From FILE)

require
file_exists: exists

feature -- Measurement

count: INTEGER

-- Number of bytes in current file;
-- Return -1 if the number of bytes was not available,
-- if the file did not exist for example.

-- (From KI_FILE)

require
is_closed: is_closed
ensure
valid_values: Result = -1 or Result >= 0
old_count: INTEGER

-- Size in bytes (0 if no associated physical file)

-- (From KL_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 LINEAR)

before: BOOLEAN

-- Is there no valid cursor position to the left of cursor position?

-- (From BILINEAR)

changeable_comparison_criterion: BOOLEAN

-- May object_comparison be changed?
-- (Answer: yes by default.)

-- (From CONTAINER)

empty: BOOLEAN

-- Is there no element?

-- (From CONTAINER)

obsolete

ELKS 2000: Use is_empty instead

exhausted: BOOLEAN

-- Has structure been completely explored?

-- (From LINEAR)

ensure
exhausted_when_off: off implies Result
exists: BOOLEAN

-- Does file physically exist on disk?
-- (Note that with SmartEiffel this routine
-- actually returns is_readable.)

-- (From KI_FILE_SYSTEM_ENTRY)

extendible: BOOLEAN

-- May new items be added?

-- (From KL_OUTPUT_FILE)

file_prunable: BOOLEAN

-- May items be removed?

-- (From FILE)

obsolete

Use prunable instead.

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 structure filled to capacity?

-- (From BOX)

is_access_executable: BOOLEAN

-- Is file executable by real UID?

-- (From FILE)

require
file_exists: exists
is_access_owner: BOOLEAN

-- Is file owned by real UID?

-- (From FILE)

require
file_exists: exists
is_access_readable: BOOLEAN

-- Is file readable by real UID?

-- (From FILE)

require
file_exists: exists
is_access_writable: BOOLEAN

-- Is file writable by real UID?

-- (From FILE)

require
file_exists: exists
is_block: BOOLEAN

-- Is file a block special file?

-- (From FILE)

require
file_exists: exists
is_character: BOOLEAN

-- Is file a character special file?

-- (From FILE)

require
file_exists: exists
is_closable: BOOLEAN

-- Can current file system entry be closed?

-- (From KI_FILE_SYSTEM_ENTRY)

ensure
definition: Result = is_open
is_closed: BOOLEAN

-- Is file closed?

-- (From KI_FILE_SYSTEM_ENTRY)

ensure
definition: Result = not is_open
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
file_exists: exists
is_directory: BOOLEAN

-- Is file a directory?

-- (From FILE)

require
file_exists: exists
is_empty: BOOLEAN

-- Is structure empty?

-- (From CONTAINER)

is_executable: BOOLEAN

-- Is file executable?
-- (Checks execute permission for effective UID.)

-- (From IO_MEDIUM)

require
handle_exists: exists
is_fifo: BOOLEAN

-- Is file a named pipe?

-- (From FILE)

require
file_exists: exists
is_inserted (v: CHARACTER): BOOLEAN

-- Has v been inserted by the most recent insertion?
-- (By default, the value returned is equivalent to calling
-- has (v). However, descendants might be able to provide more
-- efficient implementations.)

-- (From COLLECTION)

is_open_append: BOOLEAN

-- Is file open for appending?

-- (From KL_OUTPUT_FILE)

is_open_write: BOOLEAN

-- Is file opened in write mode?

-- (From KI_FILE_SYSTEM_ENTRY)

is_owner: BOOLEAN

-- Is file owned by effective UID?

-- (From FILE)

require
file_exists: exists
is_plain: BOOLEAN

-- Is file a plain file?

-- (From KL_FILE)

require
file_exists: old_exists
is_plain_text: BOOLEAN

-- Is file reserved for text (character sequences)?

-- (From IO_MEDIUM)

is_readable: BOOLEAN

-- Can file be opened in read mode?

-- (From KI_FILE_SYSTEM_ENTRY)

ensure
exists: Result implies exists
is_setgid: BOOLEAN

-- Is file setgid?

-- (From FILE)

require
file_exists: exists
is_setuid: BOOLEAN

-- Is file setuid?

-- (From FILE)

require
file_exists: exists
is_socket: BOOLEAN

-- Is file a named socket?

-- (From FILE)

require
file_exists: exists
is_sticky: BOOLEAN

-- Is file sticky (for memory swaps)?

-- (From FILE)

require
file_exists: exists
is_symlink: BOOLEAN

-- Is file a symbolic link?

-- (From FILE)

require
file_exists: exists
is_writable: BOOLEAN

-- Is file writable?
-- (Checks write permission for effective UID.)

-- (From IO_MEDIUM)

require
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 TRAVERSABLE)

old_end_of_file: BOOLEAN

-- Has an EOF been detected?

-- (From FILE)

require
opened: not is_closed
old_exists: BOOLEAN

-- Does physical file exist?
-- (Uses effective UID.)

-- (From KL_FILE)

old_is_closed: BOOLEAN

-- Is file closed?

-- (From KL_FILE)

old_is_open_read: BOOLEAN

-- Is file open for reading?

-- (From IO_MEDIUM)

old_is_open_write: BOOLEAN

-- Is file open for writing?

-- (From KL_OUTPUT_FILE)

old_is_readable: BOOLEAN

-- Is file readable?
-- (Checks permission for effective UID.)

-- (From KL_FILE)

require
file_exists: old_exists
path_exists: BOOLEAN

-- Does physical file name exist without resolving
-- symbolic links?

-- (From FILE)

ensure then
unchanged_mode: mode = old mode
prunable: BOOLEAN

-- Is there an item to be removed?

-- (From COLLECTION)

readable: BOOLEAN

-- Is there a current item that may be read?

-- (From ACTIVE)

same_physical_file (other_name: STRING): BOOLEAN

-- Are current file and file named other_name
-- the same physical file? Return False if one
-- or both files don't exist. (Return True if
-- it was impossible to determine whether the
-- files were physically the same files.)
-- (other_name should follow the pathname convention
-- of the underlying platform. For pathname conversion
-- use KI_FILE_SYSTEM.pathname_from_file_system.)

-- (From KI_FILE)

require
other_name_not_void: other_name /= Void
is_closed: is_closed
support_storable: BOOLEAN

-- Can medium be used to an Eiffel structure?

-- (From IO_MEDIUM)

writable: BOOLEAN

-- Is there a current item that may be modified?

-- (From ACTIVE)

feature {NONE} -- Status report

is_in_final_collect: BOOLEAN

-- Is GC currently performing final collection
-- after execution of current program?
-- Safe to use in dispose.

-- (From DISPOSABLE)

feature -- Status setting

compare_objects

-- Ensure that future search operations will use equal
-- rather than = for comparing references.

-- (From CONTAINER)

require
changeable_comparison_criterion: changeable_comparison_criterion
ensure
compare_references

-- Ensure that future search operations will use =
-- rather than equal for comparing references.

-- (From CONTAINER)

require
changeable_comparison_criterion: changeable_comparison_criterion
ensure
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
is_closed: is_closed
ensure
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
exists: exists
open_append: is_open_append
fd_open_read (fd: INTEGER)

-- Open file of descriptor fd in read-only mode.

-- (From FILE)

ensure
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
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
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
exists: exists
open_write: is_open_write
old_close

-- Close file.

-- (From KL_FILE)

require
medium_is_open: not old_is_closed
ensure
is_closed: old_is_closed
old_open_append

-- Open file in append-only mode;
-- create it if it does not exist.

-- (From KL_OUTPUT_FILE)

require
is_closed: old_is_closed
ensure
exists: old_exists
open_append: is_open_append
old_open_read

-- Open file in read-only mode.

-- (From FILE)

require
is_closed: is_closed
ensure
exists: exists
open_read: is_open_read
old_open_write

-- Open file in write-only mode;
-- create it if it does not exist.

-- (From KL_OUTPUT_FILE)

require
is_closed: old_is_closed
ensure
exists: old_exists
open_write: old_is_open_write
open_read_append

-- Open file in read and write-at-end mode;
-- create it if it does not exist.

-- (From FILE)

require
is_closed: is_closed
ensure
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
is_closed: is_closed
ensure
exists: exists
open_read: is_open_read
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
is_open: not is_closed
valid_name: fname /= Void
ensure
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
is_open: not is_closed
valid_name: fname /= Void
ensure
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
is_open: not is_closed
valid_name: fname /= Void
ensure
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
is_open: not is_closed
valid_name: fname /= Void
ensure
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
is_open: not is_closed
valid_name: fname /= Void
ensure
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
is_open: not is_closed
valid_name: fname /= Void
ensure
exists: exists
open_write: is_open_write

feature -- Cursor movement

back

-- Go back one position.

-- (From BILINEAR)

require
not_before: not before
finish

-- Go to last position.

-- (From LINEAR)

require else
file_opened: not is_closed
forth

-- Go to next position.

-- (From LINEAR)

require
not_after: not after
require else
file_opened: not is_closed
go (abs_position: INTEGER)

-- Go to the absolute position.
-- (New position may be beyond physical length.)

-- (From FILE)

require
file_opened: not is_closed
non_negative_argument: abs_position >= 0
move (offset: INTEGER)

-- Advance by offset from current location.

-- (From FILE)

require
file_opened: not is_closed
next_line

-- Move to next input line.

-- (From FILE)

require
is_readable: file_readable
recede (abs_position: INTEGER)

-- Go to the absolute position backwards,
-- starting from end of file.

-- (From FILE)

require
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 LINEAR)

ensure
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 TRAVERSABLE)

require else
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
who_is_not_void: who /= Void
what_is_not_void: what /= Void
file_descriptor_exists: exists
basic_store (object: ANY)

-- Produce an external representation of the
-- entire object structure reachable from object.
-- Retrievable within current system only.

-- (From IO_MEDIUM)

require
object_not_void: object /= Void
extendible: extendible
support_storable: support_storable
change_date: INTEGER

-- Time stamp of last change.

-- (From FILE)

require
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
file_exists: exists
change_mode (mask: INTEGER)

-- Replace mode by mask.

-- (From FILE)

require
file_exists: exists
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
file_exists: exists
extend (v: CHARACTER)

-- Include v at end.

-- (From COLLECTION)

require
extendible: extendible
ensure
item_inserted: is_inserted (v)
ensure then
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
other_not_void: other /= Void
extendible: extendible
force (v: like item)

-- Add v to end.

-- (From SEQUENCE)

require
extendible: extendible
ensure then
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).
--| This feature may use a visible name of a class written
--| in the visible clause of the Ace file. This makes it
--| possible to overcome class name clashes.

-- (From IO_MEDIUM)

require
object_not_void: object /= Void
extendible: extendible
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 IO_MEDIUM)

require
object_not_void: object /= Void
extendible: extendible
support_storable: support_storable
link (fn: STRING)

-- Link current file to fn.
-- fn must not already exist.

-- (From FILE)

require
file_exists: exists
new_line

-- Write a new line character at current position.

-- (From IO_MEDIUM)

require
extendible: extendible
old_append (f: like Current)

-- Append a copy of the contents of f.

-- (From SEQUENCE)

require
argument_not_void: s /= Void
require else
target_is_closed: is_closed
source_is_closed: f.is_closed
ensure
new_count: count >= old count
ensure then
new_count: count = old count + f.count
files_closed: f.is_closed and is_closed
old_change_name (new_name: STRING)

-- Change file name to new_name

-- (From KL_FILE)

require
new_name_not_void: new_name /= Void
file_exists: old_exists
ensure
name_changed: string_name.is_equal (new_name)
old_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 KL_OUTPUT_FILE)

require
is_open: not old_is_closed
old_put_character (c: CHARACTER)

-- Write c at current position.

-- (From KL_OUTPUT_FILE)

require
extendible: extendible
old_put_new_line

-- Write a new line character at current position.

-- (From IO_MEDIUM)

require
extendible: extendible
old_put_string (s: STRING)

-- Write s at current position.

-- (From KL_OUTPUT_FILE)

require
extendible: extendible
non_void: s /= void
put (v: like item)

-- Add v to end.

-- (From COLLECTION)

require
extendible: extendible
ensure
item_inserted: is_inserted (v)
ensure then
new_count: count = old count + 1
put_managed_pointer (p: MANAGED_POINTER; start_pos, nb_bytes: INTEGER)

-- Put data of length nb_bytes pointed by start_pos index in p at
-- current position.

-- (From IO_MEDIUM)

require
p_not_void: p /= Void
p_large_enough: p.count >= nb_bytes + start_pos
extendible: extendible
putchar (c: CHARACTER)

-- Write c at current position.

-- (From IO_MEDIUM)

require
extendible: extendible
putstring (s: STRING)

-- Write s at current position.

-- (From IO_MEDIUM)

require
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
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
file_exists: exists
ensure
acess_date_updated: access_date = time
date_unchanged: date = old date
set_date (time: INTEGER)

-- Stamp with time (modification time only).

-- (From FILE)

require
file_exists: exists
ensure
access_date_unchanged: access_date = old access_date
date_updated: date = time
stamp (time: INTEGER)

-- Stamp with time (for both access and modification).

-- (From FILE)

require
file_exists: exists
ensure
date_updated: date = time
touch

-- Update time stamp (for both access and modification).

-- (From FILE)

require
file_exists: exists
ensure
date_changed: date /= old date

feature -- Removal

dispose

-- Ensure this medium is closed when garbage collected.

-- (From DISPOSABLE)

old_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 KL_FILE)

require
exists: exists
old_reset (fn: STRING)

-- Change file name to fn and reset
-- file descriptor and all information.

-- (From FILE)

require
valid_file_name: fn /= Void
ensure
file_renamed: name = fn
file_closed: is_closed
prune_all (v: like item)

-- Remove all occurrences of v; go off.

-- (From COLLECTION)

require
prunable: prunable
ensure
no_more_occurrences: not has (v)
wipe_out

-- Remove all items.

-- (From COLLECTION)

require
prunable: prunable
require else
is_closed: is_closed
ensure
wiped_out: is_empty

feature -- Conversion

linear_representation: LINEAR [CHARACTER]

-- Representation as a linear structure

-- (From CONTAINER)

feature -- Basic operations

change_name (new_name: STRING)

-- Rename current file as new_name.
-- Do nothing if the file could not be renamed, if
-- it did not exist or if new_name is physically
-- the same file as current file. Overwrite new_name
-- if it already existed. If renaming was successful,
-- then name is set to new_name.
-- (new_name should follow the pathname convention
-- of the underlying platform. For pathname conversion
-- use KI_FILE_SYSTEM.pathname_from_file_system.)

-- (From KI_FILE)

require
new_name_not_void: new_name /= Void
is_closed: is_closed
close

-- Close current file if it is closable,
-- let it open otherwise.

-- (From KI_FILE_SYSTEM_ENTRY)

require
is_closable: is_closable
concat (a_filename: STRING)

-- Copy content of file a_filename to the end of current file.
-- Do nothing if file a_filename does not exist. Create
-- current file if it does not exist yet. If file a_filename
-- is physically the same as current file, then a copy of
-- the file is appended to itself. Do nothing if current
-- file could not be open in append mode or if file a_filename
-- could not be opened in read mode.
-- (a_filename should follow the pathname convention
-- of the underlying platform. For pathname conversion
-- use KI_FILE_SYSTEM.pathname_from_file_system.)

-- (From KI_FILE)

require
a_filename_not_void: a_filename /= Void
is_closed: is_closed
copy_file (new_name: STRING)

-- Copy current file to new_name.
-- Do nothing if the file could not be copied, if it
-- did not exist or if new_name is physically
-- the same file as current file. Overwrite new_name
-- if it already existed.
-- (new_name should follow the pathname convention
-- of the underlying platform. For pathname conversion
-- use KI_FILE_SYSTEM.pathname_from_file_system.)

-- (From KI_FILE)

require
new_name_not_void: new_name /= Void
is_closed: is_closed
delete

-- Delete current file.
-- Do nothing if the file could not be
-- deleted or if it did not exist.

-- (From KI_FILE_SYSTEM_ENTRY)

require
is_closed: is_closed
flush

-- Flush buffered data to disk.

-- (From KI_CHARACTER_OUTPUT_STREAM)

require
is_open_write: is_open_write
open_append

-- Open current file in append mode if it
-- can be opened, let it closed otherwise.
-- If the file is successfully opened, it is
-- either created if it didn't exist or the
-- data which will be written to the file will
-- appear after its old content otherwise.

-- (From KI_OUTPUT_FILE)

require
is_closed: is_closed
open_write

-- Open current file in write-only mode if
-- it can be opened, let it closed otherwise.
-- If the file is successfully opened, it is
-- either created if it didn't exist or its
-- old content is removed otherwise.

-- (From KI_FILE_SYSTEM_ENTRY)

require
is_closed: is_closed
recursive_open_append

-- Open current file in append mode if it
-- can be opened, let it closed otherwise.
-- If the file is successfully opened, it is
-- either created if it didn't exist or the
-- data which will be written to the file will
-- appear after its old content otherwise.
-- Try to recursively create its parent directory
-- if it does not exist yet.

-- (From KI_OUTPUT_FILE)

require
is_closed: is_closed
recursive_open_write

-- Open current file in write-only mode if
-- it can be opened, let it closed otherwise.
-- If the file is successfully opened, it is
-- either created if it didn't exist or its
-- old content is removed otherwise. Try to
-- recursively create its parent directory
-- if it does not exist yet.

-- (From KI_OUTPUT_FILE)

require
is_closed: is_closed

feature -- Iteration

do_all (action: PROCEDURE [ANY, TUPLE [CHARACTER]])

-- Apply action to every item.
-- Semantics not guaranteed if action changes the structure;
-- in such a case, apply iterator to clone of structure instead.

-- (From TRAVERSABLE)

require
action_exists: action /= Void
do_if (action: PROCEDURE [ANY, TUPLE [CHARACTER]]test: FUNCTION [ANY, TUPLE [CHARACTER], BOOLEAN])

-- Apply action to every item that satisfies test.
-- Semantics not guaranteed if action or test changes the structure;
-- in such a case, apply iterator to clone of structure instead.

-- (From TRAVERSABLE)

require
action_exists: action /= Void
test_exits: test /= Void
for_all (test: FUNCTION [ANY, TUPLE [CHARACTER], BOOLEAN]): BOOLEAN

-- Is test true for all items?

-- (From TRAVERSABLE)

require
test_exits: test /= Void
ensure then
empty: is_empty implies Result
there_exists (test: FUNCTION [ANY, TUPLE [CHARACTER], BOOLEAN]): BOOLEAN

-- Is test true for at least one item?

-- (From TRAVERSABLE)

require
test_exits: test /= Void

feature -- Input

old_read_character

-- Read a new character.
-- Make result available in last_character.

-- (From IO_MEDIUM)

require
is_readable: readable
require else
is_readable: file_readable
old_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.

-- (From IO_MEDIUM)

require
is_readable: readable
require else
is_readable: file_readable
old_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.

-- (From IO_MEDIUM)

require
is_readable: readable
require else
is_readable: file_readable
read_data (p: POINTER; nb_bytes: INTEGER)

-- Read a string of at most nb_bytes bound bytes
-- or until end of file.
-- Make result available in p.

-- (From RAW_FILE)

obsolete

require
p_not_null: p /= default_pointer
is_readable: file_readable
read_double

-- Read the binary representation of a new double
-- from file. Make result available in last_double.

-- (From IO_MEDIUM)

require
is_readable: readable
require else
is_readable: file_readable
read_integer

-- Read the binary representation of a new integer
-- from file. Make result available in last_integer.

-- (From IO_MEDIUM)

require
is_readable: readable
require else
is_readable: file_readable
read_real

-- Read the binary representation of a new real
-- from file. Make result available in last_real.

-- (From IO_MEDIUM)

require
is_readable: readable
require else
is_readable: file_readable
read_to_managed_pointer (p: MANAGED_POINTER; start_pos, nb_bytes: INTEGER)

-- Read at most nb_bytes bound bytes and make result
-- available in p at position start_pos.

-- (From IO_MEDIUM)

require
p_not_void: p /= Void
p_large_enough: p.count >= nb_bytes + start_pos
is_readable: readable
require else
p_not_void: p /= Void
p_large_enough: p.count >= nb_bytes + start_pos
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.

-- (From FILE)

require
is_readable: file_readable
readchar

-- Read a new character.
-- Make result available in last_character.

-- (From IO_MEDIUM)

require
is_readable: readable
require else
is_readable: file_readable
readdouble

-- Read the binary representation of a new double
-- from file. Make result available in last_double.

-- (From IO_MEDIUM)

require
is_readable: readable
require else
is_readable: file_readable
readint

-- Read the binary representation of a new integer
-- from file. Make result available in last_integer.

-- (From IO_MEDIUM)

require
is_readable: readable
require else
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.

-- (From IO_MEDIUM)

require
is_readable: readable
require else
is_readable: file_readable
readreal

-- Read the binary representation of a new real
-- from file. Make result available in last_real.

-- (From IO_MEDIUM)

require
is_readable: readable
require else
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.

-- (From IO_MEDIUM)

require
is_readable: readable
require else
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.

-- (From FILE)

require
is_readable: file_readable

feature -- Output

append (an_input_stream: KI_INPUT_STREAM [CHARACTER])

-- Read items of an_input_stream until the end
-- of input is reached, and write these items to
-- current output stream.

-- (From KI_OUTPUT_STREAM)

require
is_open_write: is_open_write
an_input_stream_not_void: an_input_stream /= Void
an_input_stream_open_read: an_input_stream.is_open_read
ensure
end_of_input: an_input_stream.end_of_input
old_put_boolean (b: BOOLEAN)

-- Write binary value of b at current position.

-- (From IO_MEDIUM)

require
extendible: extendible
old_put_integer (i: INTEGER)

-- Write binary value of i at current position.

-- (From IO_MEDIUM)

require
extendible: extendible
put_boolean (b: BOOLEAN)

-- Write "True" to output stream if
-- b is true, "False" otherwise.

-- (From KI_CHARACTER_OUTPUT_STREAM)

require
is_open_write: is_open_write
put_character (c: CHARACTER)

-- Write c to output file.

-- (From KI_OUTPUT_STREAM)

require
is_open_write: is_open_write
put_data (p: POINTER; size: INTEGER)

-- Put data of length size pointed by p at
-- current position.

-- (From RAW_FILE)

obsolete

Use put_managed_pointer instead.

require
p_not_null: p /= default_pointer
extendible: extendible
put_double (d: DOUBLE)

-- Write binary value d at current position.

-- (From IO_MEDIUM)

require
extendible: extendible
put_integer (i: INTEGER)

-- Write decimal representation
-- of i to output stream.
-- Regexp: 0|(-?[1-9][0-9]*)

-- (From KI_CHARACTER_OUTPUT_STREAM)

require
is_open_write: is_open_write
put_line (a_string: STRING)

-- Write a_string to output stream
-- followed by a line separator.

-- (From KI_TEXT_OUTPUT_STREAM)

require
is_open_write: is_open_write
a_string_not_void: a_string /= Void
put_new_line

-- Write a line separator to output stream.

-- (From KI_TEXT_OUTPUT_STREAM)

require
is_open_write: is_open_write
put_real (r: REAL)

-- Write binary value of r at current position.

-- (From IO_MEDIUM)

require
extendible: extendible
put_string (a_string: STRING)

-- Write a_string to output file.
-- Note: If a_string is a UC_STRING or descendant, then
-- write the bytes of its associated UTF unicode encoding.

-- (From KI_CHARACTER_OUTPUT_STREAM)

require
is_open_write: is_open_write
a_string_not_void: a_string /= Void
put_substring (a_string: STRING; s, e: INTEGER)

-- Write substring of a_string between indexes
-- s and e to output stream.

-- (From KI_CHARACTER_OUTPUT_STREAM)

require
is_open_write: is_open_write
a_string_not_void: a_string /= Void
s_large_enough: s >= 1
e_small_enough: e <= a_string.count
valid_interval: s <= e + 1
putbool (b: BOOLEAN)

-- Write binary value of b at current position.

-- (From IO_MEDIUM)

require
extendible: extendible
putdouble (d: DOUBLE)

-- Write binary value d at current position.

-- (From IO_MEDIUM)

require
extendible: extendible
putint (i: INTEGER)

-- Write binary value of i at current position.

-- (From IO_MEDIUM)

require
extendible: extendible
putreal (r: REAL)

-- Write binary value of r at current position.

-- (From IO_MEDIUM)

require
extendible: extendible

feature -- Convenience

copy_to (file: like Current)

-- Copy content of current from current cursor
-- position to end of file into file from
-- current cursor position of file.

-- (From FILE)

require
file_not_void: file /= Void
file_is_open_write: file.is_open_write
current_is_open_read: is_open_read

feature -- Acess

operating_system: KL_OPERATING_SYSTEM

-- Underlying operating system

-- (From KL_SHARED_OPERATING_SYSTEM)

ensure
operating_system_not_void: Result /= Void

feature -- File systems

file_system: KL_FILE_SYSTEM

-- Underlying file system

-- (From KL_SHARED_FILE_SYSTEM)

ensure
file_system_not_void: Result /= Void
current_file_system: Result.is_current_file_system
unix_file_system: KL_UNIX_FILE_SYSTEM

-- Unix-like file system

-- (From KL_SHARED_FILE_SYSTEM)

ensure
file_system_not_void: Result /= Void
windows_backslash_only_file_system: KL_WINDOWS_FILE_SYSTEM

-- Windows-like file system which accepts only \ as
-- directory separator

-- (From KL_SHARED_FILE_SYSTEM)

ensure
file_system_not_void: Result /= Void
windows_file_system: KL_WINDOWS_FILE_SYSTEM

-- Windows-like file system which accepts both
-- \ and / as directory separator

-- (From KL_SHARED_FILE_SYSTEM)

ensure
file_system_not_void: Result /= Void

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)

feature {NONE} -- Inapplicable

go_to (r: CURSOR)

-- Move to position marked r.

-- (From FILE)

prune (v: like item)

-- Remove an occurrence of v if any.

-- (From COLLECTION)

require
prunable: prunable
ensure then
count <= old count
remove

-- Remove current item.

-- (From ACTIVE)

require
prunable: prunable
writable: writable
replace (v: like item)

-- Replace current item by v.

-- (From ACTIVE)

require
writable: writable
require else
is_writable: file_writable
ensure
item_replaced: item = v
ensure then
item = vcount = old count

feature {NONE} -- Implementation

empty_name: STRING

-- Empty name place-holder

-- (From KL_FILE)

false_constant: STRING

-- String representation of boolean values

-- (From KI_CHARACTER_OUTPUT_STREAM)

buffered_file_info: UNIX_FILE_INFO

-- Information about the file.

-- (From FILE)

c_basic_store (file_handle: INTEGER; object: POINTER)

-- Store object structure reachable form current object
-- in file pointer file_ptr.

-- (From FILE)

c_general_store (file_handle: INTEGER; object: POINTER)

-- Store object structure reachable form current object
-- in file pointer file_ptr.

-- (From FILE)

c_independent_store (file_handle: INTEGER; object: POINTER)

-- Store object structure reachable form current object
-- in file pointer file_ptr.

-- (From FILE)

c_retrieved (file_handle: INTEGER): ANY

-- Object structured retrieved from file of pointer
-- file_ptr

-- (From FILE)

create_last_string (a_min_size: INTEGER)

-- Create new instance of last_string with a least a_min_size
-- as capacity.

-- (From FILE)

require
last_string_void: last_string = Void
a_min_size_non_negative: a_min_size >= 0
ensure
last_string_not_void: last_string /= Void
capacity_set: last_string.capacity >= a_min_size
default_last_string_size: INTEGER

-- Default size for creating last_string

-- (From FILE)

dummy_name: STRING

-- Dummy name

-- (From KL_FILE)

false_string: STRING

-- Character string "false"

-- (From FILE)

file_access (f_name: POINTER; which: INTEGER): BOOLEAN

-- Perform access test which on f_name using real UID.

-- (From FILE)

file_append (file, from_file: POINTER; length: INTEGER)

-- Append a copy of from_file to file

-- (From FILE)

file_chgrp (f_name: POINTER; new_group: INTEGER)

-- Change group of f_name to new_group

-- (From FILE)

file_chmod (f_name: POINTER; mask: INTEGER)

-- Change mode of f_name to mask.

-- (From FILE)

file_chown (f_name: POINTER; new_owner: INTEGER)

-- Change owner of f_name to new_owner

-- (From FILE)

file_close (file: POINTER)

-- Close file.

-- (From FILE)

file_creatable (f_name: POINTER; n: INTEGER): BOOLEAN

-- Is f_name of count n creatable.

-- (From FILE)

file_dopen (fd, how: INTEGER): POINTER

-- File pointer for file of descriptor fd in mode how
-- (which must fit the way fd was obtained).

-- (From FILE)

file_exists (f_name: POINTER): BOOLEAN

-- Does f_name exist.

-- (From FILE)

file_fd (file: POINTER): INTEGER

-- Operating system's file descriptor

-- (From FILE)

file_feof (file: POINTER): BOOLEAN

-- End of file?

-- (From FILE)

file_flush (file: POINTER)

-- Flush file.

-- (From FILE)

file_fread (dest: POINTER; elem_size, nb_elems: INTEGER; file: POINTER): INTEGER

-- Read nb_elems of size elem_size in file file and store them
-- in location dest.

-- (From RAW_FILE)

file_gc (file: POINTER): CHARACTER

-- Access the next character

-- (From FILE)

file_gdb (file: POINTER): DOUBLE

-- Read a double from file

-- (From RAW_FILE)

file_gib (file: POINTER): INTEGER

-- Get an integer from file

-- (From RAW_FILE)

file_go (file: POINTER; abs_position: INTEGER)

-- Go to absolute position, originated from start.

-- (From FILE)

file_grb (file: POINTER): REAL

-- Read a real from file

-- (From RAW_FILE)

file_gs (file: POINTER; a_string: POINTER; length, begin: INTEGER): INTEGER

-- a_string updated with characters read from file
-- until new line, with begin characters already read.
-- If it does not fit, result is length - begin + 1.
-- If it fits, result is number of characters read.

-- (From FILE)

file_gss (file: POINTER; a_string: POINTER; length: INTEGER): INTEGER

-- Read min (length, remaining bytes in file) characters
-- into a_string. If it does not fit, result is length + 1.
-- Otherwise, result is the number of characters read.

-- (From FILE)

file_gw (file: POINTER; a_string: POINTER; length, begin: INTEGER): INTEGER

-- Read a string excluding white space and stripping
-- leading white space from file into a_string.
-- White space characters are: blank, new_line,
-- tab, vertical tab, formfeed or end of file.
-- If it does not fit, result is length - begin + 1,
-- otherwise result is number of characters read.

-- (From FILE)

file_lh (file: POINTER): CHARACTER

-- Look ahead in file and find out the value of the next
-- character. Do not read over character.

-- (From FILE)

file_link (from_name, to_name: POINTER)

-- Link to_name to from_name

-- (From FILE)

file_move (file: POINTER; offset: INTEGER)

-- Move file pointer by offset.

-- (From FILE)

file_open (f_name: POINTER; how: INTEGER): POINTER

-- File pointer for file f_name, in mode how.

-- (From FILE)

file_path_exists (f_name: POINTER): BOOLEAN

-- Does f_name exist.

-- (From FILE)

file_pc (file: POINTER; c: CHARACTER)

-- Put c to end of file.

-- (From FILE)

file_pdb (file: POINTER; d: DOUBLE)

-- Put d to end of file.

-- (From RAW_FILE)

file_perm (f_name, who, what: POINTER; flag: INTEGER)

-- Change permissions for f_name to who and what.
-- flag = 1 -> add permissions,
-- flag = 0 -> remove permissions.

-- (From FILE)

file_pib (file: POINTER; n: INTEGER)

-- Put n to end of file.

-- (From RAW_FILE)

file_prb (file: POINTER; r: REAL)

-- Put r to end of file.

-- (From RAW_FILE)

file_ps (file: POINTER; a_string: POINTER; length: INTEGER)

-- Print a_string to file.

-- (From FILE)

file_recede (file: POINTER; abs_position: INTEGER)

-- Go to absolute position, originated from end.

-- (From FILE)

file_rename (old_name, new_name: POINTER)

-- Change file name from old_name to new_name.

-- (From FILE)

file_reopen (f_name: POINTER; how: INTEGER; file: POINTER): POINTER

-- File pointer to file, reopened to have new name f_name
-- in a mode specified by how.

-- (From FILE)

file_size (file: POINTER): INTEGER

-- Size of file

-- (From FILE)

file_tell (file: POINTER): INTEGER

-- Current cursor position in file.

-- (From FILE)

file_tnil (file: POINTER)

-- Read upto next input line.

-- (From FILE)

file_tnwl (file: POINTER)

-- Print a new-line to file.

-- (From FILE)

file_touch (f_name: POINTER)

-- Touch file f_name.

-- (From FILE)

file_unlink (fname: POINTER)

-- Delete file fname.

-- (From FILE)

file_utime (f_name: POINTER; time, how: INTEGER)

-- Set access, modification time or both (how = 0,1,2) on
-- f_name, using time as time stamp.

-- (From FILE)

read_to_string (a_string: STRING; pos, nb: INTEGER): INTEGER

-- Fill a_string, starting at position pos with at
-- most nb characters read from current file.
-- Return the number of characters actually read.

-- (From FILE)

require
is_readable: file_readable
not_end_of_file: not end_of_file
a_string_not_void: a_string /= Void
valid_position: a_string.valid_index (pos)
nb_large_enough: nb > 0
nb_small_enough: nb <= a_string.count - pos + 1
ensure
nb_char_read_large_enough: Result >= 0
nb_char_read_small_enough: Result <= nb
character_read: not end_of_file implies Result > 0
set_buffer

-- Resynchronizes information on file

-- (From FILE)

require
file_exists: exists
string_name: STRING

-- Name of file (STRING version)

-- (From KL_FILE)

tmp_file1: KL_TEXT_INPUT_FILE

-- Temporary file object

-- (From KL_FILE)

ensure
file_not_void: Result /= Void
file_closed: Result.is_closed
true_string: STRING

-- Character string "true"

-- (From FILE)

feature {FILE} -- Implementation

append_read_file: INTEGER

-- (From FILE)

append_file: INTEGER

-- (From FILE)

closed_file: INTEGER

-- (From FILE)

read_write_file: INTEGER

-- (From FILE)

read_file: INTEGER

-- (From FILE)

write_file: INTEGER

-- (From FILE)

mode: INTEGER

-- Input-output mode

-- (From FILE)

set_read_mode

-- Define file mode as read.

-- (From FILE)

set_write_mode

-- Define file mode as write.

-- (From FILE)

invariant


-- From ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)

-- From KL_FILE
string_name_is_string: ANY_.same_types (string_name,
)

-- From RAW_FILE
not_plain_text: not is_plain_text

-- From FILE
valid_mode: Closed_file <= mode and mode <= Append_read_file
name_exists: name /= Void
name_not_empty: not name.is_empty

-- From FINITE
empty_definition: is_empty = (count = 0)
non_negative_count: count >= 0

-- From ACTIVE
writable_constraint: writable implies readable
empty_constraint: is_empty implies (not readable) and (not writable)

-- From BILINEAR
not_both: not (after and before)
before_constraint: before implies off

-- From LINEAR
after_constraint: after implies off

-- From TRAVERSABLE
empty_constraint: is_empty implies off

end