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

kernel.io

Class KL_STRING_INPUT_STREAM


Direct ancestors

KI_TEXT_INPUT_STREAM, KL_IMPORTED_STRING_ROUTINES

Known direct descendants

EM_NET_UNSERIALIZER

Creation

Features

Invariants

indexing

description

Character input streams based on strings

library

Gobo Eiffel Kernel Library

copyright

Copyright (c) 2002, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

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

revision

$Revision: 1.8 $

class

KL_STRING_INPUT_STREAM

inherit

KI_TEXT_INPUT_STREAM
KL_IMPORTED_STRING_ROUTINES

create

make (a_string: like string)

-- Create a new string input stream.

require
a_string_not_void: a_string /= Void
ensure
string_set: string = a_string

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
eol: STRING

-- Line separator

-- (From KI_TEXT_INPUT_STREAM)

ensure
eol_not_void: Result /= Void
eol_not_empty: Result.count > 0
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
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,
)
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 characters 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 character in input stream.
-- 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_line

-- Read characters from input stream until a line separator
-- or end of input is reached. Make the characters that have
-- been read available in last_string and discard the line
-- separator characters from the input steam.

-- (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 stream.
-- Make the characters making up the recognized
-- line separator available in last_string,
-- or make last_string empty and leave the
-- input stream 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
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 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.

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

string_not_void: string /= Void
location_positive: location >= 0

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

end