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

kernel.spec.ise

Class KL_INPUT_STREAM_ROUTINES


Direct ancestors

KL_IMPORTED_INPUT_STREAM_ROUTINES, KL_IMPORTED_ANY_ROUTINES

Features

Invariants

indexing

description

Routines that ought to be in class INPUT_STREAM

library

Gobo Eiffel Kernel Library

copyright

Copyright (c) 1999, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2005/02/07 16:21:59 $

revision

$Revision: 1.6 $

class

KL_INPUT_STREAM_ROUTINES

obsolete

[020502] Use descendants of KI_INPUT_STREAM instead.

inherit

KL_IMPORTED_INPUT_STREAM_ROUTINES
KL_IMPORTED_ANY_ROUTINES

feature -- Initialization

make_file_open_read (a_filename: STRING): like INPUT_STREAM_TYPE

-- Create a new file object with a_filename as
-- file name and try to open it in read-only mode.
-- is_open_read (Result) is set to True
-- if operation was successful.

require
a_filename_not_void: a_filename /= Void
a_filename_is_string: ANY_.same_types (a_filename,
)
a_filename_not_empty: a_filename.count > 0
ensure
file_not_void: Result /= Void

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
input_stream_: KL_INPUT_STREAM_ROUTINES

-- Routines that ought to be in class INPUT_STREAM

-- (From KL_IMPORTED_INPUT_STREAM_ROUTINES)

ensure
input_stream_routines_not_void: Result /= Void
name (a_stream: like INPUT_STREAM_TYPE): STRING

-- Name of a_stream

require
a_stream_void: a_stream /= Void
ensure
name_not_void: Result /= Void

feature -- Status report

end_of_input (a_stream: like INPUT_STREAM_TYPE): BOOLEAN

-- Has an EOF been detected?

require
a_stream_void: a_stream /= Void
a_stream_is_open_read: is_open_read (a_stream)
is_closed (a_stream: like INPUT_STREAM_TYPE): BOOLEAN

-- Is a_stream closed?

require
a_stream_void: a_stream /= Void
is_open_read (a_stream: like INPUT_STREAM_TYPE): BOOLEAN

-- Is a_stream open in read mode?

require
a_stream_void: a_stream /= Void

feature -- Status setting

close (a_stream: like INPUT_STREAM_TYPE)

-- Close a_stream if it is closable,
-- let it open otherwise.

require
a_stream_not_void: a_stream /= Void
not_closed: not is_closed (a_stream)

feature -- Input operations

read_stream (a_stream: like INPUT_STREAM_TYPE;a_buffer: STRING; pos, nb_char: INTEGER): INTEGER

-- Fill a_buffer, starting at position pos with
-- at most nb_char characters read from a_stream.
-- Return the number of characters actually read.

require
a_stream_not_void: a_stream /= Void
a_stream_open_read: is_open_read (a_stream)
a_buffer_not_void: a_buffer /= Void
a_buffer_is_string: ANY_.same_types (a_buffer,
)
valid_position: a_buffer.valid_index (pos)
nb_char_large_enough: nb_char >= 0
nb_char_small_enough: nb_char <= a_buffer.count - pos + 1
ensure
nb_char_read_large_enough: Result >= 0
nb_char_read_small_enough: Result <= nb_char
read_string (a_stream: like INPUT_STREAM_TYPE; nb_char: INTEGER): STRING

-- Read at most nb_char characters read from a_stream.
-- Return the characters that have actually been read.

require
a_stream_not_void: a_stream /= Void
a_stream_open_read: is_open_read (a_stream)
nb_char_large_enough: nb_char >= 0
ensure
string_not_void: Result /= Void
string_count_small_enough: Result.count <= nb_char

feature -- Type anchors

invariant


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

end