elogger API
Overview Classes Cluster Class Index          Top Features

kernel.spec.ise

Class KL_MACOS_INPUT_FILE


Direct ancestors

KI_TEXT_INPUT_FILE, KL_BINARY_INPUT_FILE

Creation

Features

Invariants

indexing

description

MacOS-like text input 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)

class KL_MACOS_INPUT_FILE

inherit

KI_TEXT_INPUT_FILE
KI_INPUT_FILE
KI_TEXT_INPUT_STREAM
KL_BINARY_INPUT_FILE
KI_BINARY_INPUT_FILE
KL_INPUT_FILE
RAW_FILE
FILE
UNBOUNDED [CHARACTER]
FINITE
BOX
CONTAINER
SEQUENCE [CHARACTER]
ACTIVE
BAG
COLLECTION
CONTAINER
BILINEAR
LINEAR
TRAVERSABLE
CONTAINER
LINEAR
TRAVERSABLE
CONTAINER
FINITE
BOX
CONTAINER
IO_MEDIUM

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

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

last_character: CHARACTER

-- Last character read
-- (From KI_INPUT_STREAM)

require

is_open_read: is_open_read
not_end_of_input: not end_of_input

ensure then

extended_ascii: Result.code <= Platform.Maximum_byte_code

last_string: STRING

-- Last string read
-- (Note: this query always return the same object.
-- Therefore a clone should be used if the result
-- is to be kept beyond the next call to this feature.
-- However last_string is not shared between file objects.)
-- (From KI_CHARACTER_INPUT_STREAM)

require

is_open_read: is_open_read
not_end_of_input: not end_of_input

ensure

string_type: Result /= Void implies ANY_.same_types (Result, "")

Platform: KL_PLATFORM

-- Platform-dependent properties
-- (From KL_SHARED_PLATFORM)

ensure

platform_not_void: Result /= Void

ANY_: KL_ANY_ROUTINES

-- Routines that ought to be in class ANY
-- (From KL_IMPORTED_ANY_ROUTINES)

ensure

any_routines_not_void: Result /= Void

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

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

file_pointer: POINTER

-- File pointer as required in C
-- (From FILE)

eol: STRING

-- Line separator
-- (From KI_TEXT_INPUT_STREAM)

ensure

eol_not_void: Result /= Void
eol_not_empty: Result.count > 0

feature -- Measurement

old_count: INTEGER

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

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

end_of_input: BOOLEAN

-- Has the end of input stream been reached?
-- (From KI_INPUT_STREAM)

require

is_open_read: is_open_read

ensure then

definition: Result = end_of_file

valid_unread_character (a_character: CHARACTER): BOOLEAN

-- Can a_character be put back in input stream?
-- (From KI_INPUT_STREAM)

ensure then

extended_ascii: Result = (a_character.code <= Platform.Maximum_byte_code)

exists: BOOLEAN

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

is_closed: BOOLEAN

-- Is file closed?
-- (From KI_FILE_SYSTEM_ENTRY)

ensure

definition: Result = not is_open

is_readable: BOOLEAN

-- Can file 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

is_rewindable: BOOLEAN

-- Can current input stream be rewound to return input from
-- the beginning of the stream?
-- (From KI_INPUT_STREAM)

ensure

rewind_implies_open: Result implies is_open_read

is_closable: BOOLEAN

-- Can current file system entry be closed?
-- (From KI_FILE_SYSTEM_ENTRY)

ensure

definition: Result = is_open

extendible: BOOLEAN

-- May new items be added?
-- (From COLLECTION)

old_is_closed: BOOLEAN

-- Is file closed?
-- (From KL_FILE)

old_is_open_write: BOOLEAN

-- Is file open for writing?
-- (From IO_MEDIUM)

end_of_file: BOOLEAN

-- Has the end of file been reached?
-- (From KI_INPUT_FILE)

require

is_open_read: is_open_read

is_open_read: BOOLEAN

-- Is file opened in read mode?
-- (From KI_FILE_SYSTEM_ENTRY)

feature -- Status setting

old_close

-- Close file.
-- (From KL_FILE)

require

medium_is_open: not old_is_closed

ensure

is_closed: old_is_closed

old_open_read

-- Open file in read-only mode.
-- (From KL_INPUT_FILE)

require

is_closed: old_is_closed

ensure

exists: old_exists
open_read: old_is_open_read

feature -- Element change

old_put_string (s: STRING)

-- Write s at current position.
-- (From IO_MEDIUM)

require

extendible: extendible
non_void: s /= Void

feature -- Basic operations

rewind

-- Move input position to the beginning of stream.
-- (From KI_INPUT_STREAM)

require

can_rewind: is_rewindable

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

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

close

-- Close current file if it is closable,
-- let it open otherwise.
-- (From KI_FILE_SYSTEM_ENTRY)

require

is_closable: is_closable

open_read

-- Open current file in read-only mode if
-- it can be opened, let it closed otherwise.
-- (From KI_FILE_SYSTEM_ENTRY)

require

is_closed: is_closed

ensure then

not_eof: is_open_read implies not end_of_file

feature -- Input

read_character

-- Read the next character in input file.
-- Make the result available in last_character.
-- (From KI_INPUT_STREAM)

require

is_open_read: is_open_read
not_end_of_input: not end_of_input

read_string (nb: INTEGER)

-- Read at most nb characters from input stream.
-- Make the characters that have actually been read
-- available in last_string.
-- (From KI_CHARACTER_INPUT_STREAM)

require

is_open_read: is_open_read
not_end_of_input: not end_of_input
nb_large_enough: nb > 0

ensure

last_string_not_void: not end_of_input implies last_string /= Void
last_string_count_small_enough: not end_of_input implies last_string.count <= nb
character_read: not end_of_input implies last_string.count > 0

read_to_buffer (a_buffer: KI_BUFFER[CHARACTER]; pos, nb: INTEGER): INTEGER

-- Fill a_buffer, starting at position pos, with
-- at most nb characters read from input stream.
-- Return the number of characters actually read.
-- (From KI_INPUT_STREAM)

require

is_open_read: is_open_read
not_end_of_input: not end_of_input
a_buffer_not_void: a_buffer /= Void
pos_large_enough: pos >= 1
nb_large_enough: nb > 0
enough_space: (pos + nb - 1) <= a_buffer.count

ensure

nb_item_read_large_enough: Result >= 0
nb_item_read_small_enough: Result <= nb
not_end_of_input: not end_of_input implies Result > 0

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

-- Fill a_string, starting at position pos with
-- at most nb characters read from input file.
-- Return the number of characters actually read.
-- (From KI_CHARACTER_INPUT_STREAM)

require

is_open_read: is_open_read
not_end_of_input: not end_of_input
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_input implies Result > 0

unread_character (a_character: CHARACTER)

-- Put a_character back in input file.
-- This character will be read first by the next
-- call to a read routine.
-- (From KI_INPUT_STREAM)

require

is_open_read: is_open_read
an_item_valid: valid_unread_item (an_item)

ensure

not_end_of_input: not end_of_input
last_item_set: last_item = an_item

read_line

-- Read characters from input file until a line separator
-- or end of file is reached. Make the characters that have
-- been read available in last_string and discard the line
-- separator characters from the input file.
-- (From KI_TEXT_INPUT_STREAM)

require

is_open_read: is_open_read
not_end_of_input: not end_of_input

ensure

last_string_not_void: not end_of_input implies last_string /= Void

read_new_line

-- Read a line separator from input file.
-- Make the characters making up the recognized
-- line separator available in last_string,
-- or make last_string empty and leave the
-- input file unchanged if no line separator
-- was found.
-- (From KI_TEXT_INPUT_STREAM)

require

is_open_read: is_open_read
not_end_of_input: not end_of_input

ensure

not_end_of_input: not end_of_input
last_string_not_void: last_string /= Void

feature -- Obsolete

platform_: KL_PLATFORM

-- Platform-dependent properties
-- (From KL_SHARED_PLATFORM)

obsolete

[040101] Use Platform instead.

ensure

platform_not_void: Result /= Void

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

Documentation generated by edoc