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

kernel.io

Class KI_INPUT_STREAM


Known direct descendants

KI_CHARACTER_INPUT_STREAM, KI_DIRECTORY

Features

Invariants

indexing

description

Interface for 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: 2004/12/22 22:45:54 $

revision

$Revision: 1.18 $

deferred class

KI_INPUT_STREAM [G]

feature -- Access

last_item: G

-- Last item read

require
is_open_read: is_open_read
not_end_of_input: not end_of_input
name: STRING

-- Name of input stream

ensure
name_not_void: Result /= Void

feature -- Status report

end_of_input: BOOLEAN

-- Has the end of input stream been reached?

require
is_open_read: is_open_read
is_closable: BOOLEAN

-- Can current input stream be closed?

ensure
is_open: Result implies is_open_read
is_open_read: BOOLEAN

-- Can items be read from input stream?

is_rewindable: BOOLEAN

-- Can current input stream be rewound to return input from
-- the beginning of the stream?

ensure
rewind_implies_open: Result implies is_open_read
valid_unread_item (an_item: G): BOOLEAN

-- Can an_item be put back in 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.

require
is_closable: is_closable
rewind

-- Move input position to the beginning of stream.

require
can_rewind: is_rewindable

feature -- Input

read

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

require
is_open_read: is_open_read
not_end_of_input: not end_of_input
read_to_buffer (a_buffer: KI_BUFFER [G]; 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.

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

-- Put an_item back in input stream.
-- This item will be read first by the next
-- call to a read routine.

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