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

kernel.io

Class KI_BINARY_OUTPUT_FILE


Direct ancestors

KI_OUTPUT_FILE

Known direct descendants

KL_BINARY_OUTPUT_FILE

Features

Invariants

indexing

description

Interface for binary 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: 2003/02/07 12:49:50 $

revision

$Revision: 1.5 $

deferred class

KI_BINARY_OUTPUT_FILE

inherit

KI_OUTPUT_FILE

feature -- Initialization

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 -- Access

name: STRING

-- Name of output stream

-- (From KI_FILE_SYSTEM_ENTRY)

ensure
name_not_void: Result /= Void
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

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

feature -- Status report

exists: BOOLEAN

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

-- (From KI_FILE_SYSTEM_ENTRY)

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 system entry closed?

-- (From KI_FILE_SYSTEM_ENTRY)

ensure
definition: Result = not is_open
is_open_write: BOOLEAN

-- Can items be written to output stream?

-- (From KI_FILE_SYSTEM_ENTRY)

is_readable: BOOLEAN

-- Can file system entry be opened in read mode?

-- (From KI_FILE_SYSTEM_ENTRY)

ensure
exists: Result implies exists
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

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

-- Try to close output stream if it is closable. Set
-- is_open_write to false if operation was successful.

-- (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 system entry.
-- Do nothing if the entry could not be deleted
-- (for example if the entry does not exist or
-- if a directory is not empty).

-- (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

-- Try to open file system entry. Set is_open
-- to true if operation was successful.

-- (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 -- 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
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 (v: CHARACTER)

-- Write v to output stream.

-- (From KI_OUTPUT_STREAM)

require
is_open_write: is_open_write
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_string (a_string: STRING)

-- Write a_string to output stream.

-- (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

invariant


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

end