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

kernel.io

Class KI_CHARACTER_INPUT_STREAM


Direct ancestors

KI_INPUT_STREAM, KL_IMPORTED_ANY_ROUTINES

Known direct descendants

KI_INPUT_FILE, KI_TEXT_INPUT_STREAM, KL_PROXY_CHARACTER_INPUT_STREAM, XM_EIFFEL_INPUT_STREAM

Features

Invariants

indexing

description

Interface for character input streams

library

Gobo Eiffel Kernel Library

copyright

Copyright (c) 2001, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

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

revision

$Revision: 1.10 $

deferred class

KI_CHARACTER_INPUT_STREAM

inherit

KI_INPUT_STREAM
KL_IMPORTED_ANY_ROUTINES

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
last_character: CHARACTER

-- Last item read

-- (From KI_INPUT_STREAM)

require
is_open_read: is_open_read
not_end_of_input: not end_of_input
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.)

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,
)
name: STRING

-- Name of input stream

-- (From KI_INPUT_STREAM)

ensure
name_not_void: Result /= Void

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
is_closable: BOOLEAN

-- Can current input stream be closed?

-- (From KI_INPUT_STREAM)

ensure
is_open: Result implies is_open_read
is_open_read: BOOLEAN

-- Can items be read from input stream?

-- (From KI_INPUT_STREAM)

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
valid_unread_character (a_character: CHARACTER): BOOLEAN

-- Can a_character be put back in input stream?

-- (From KI_INPUT_STREAM)

feature -- Basic operations

close

-- Try to close input stream if it is closable. Set
-- is_open_read to false if operation was successful.

-- (From KI_INPUT_STREAM)

require
is_closable: is_closable
rewind

-- Move input position to the beginning of stream.

-- (From KI_INPUT_STREAM)

require
can_rewind: is_rewindable

feature -- Input

read_character

-- Read the next item in input stream.
-- Make the result available in last_item.

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

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 items read from input stream.
-- Return the number of items 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 stream.
-- Return the number of characters actually read.

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

-- Put an_item back in input stream.
-- This item 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

invariant


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

end