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

xml.parser.eiffel

Class XM_EIFFEL_INPUT_STREAM


Direct ancestors

KI_CHARACTER_INPUT_STREAM, KL_SHARED_STANDARD_FILES, KL_IMPORTED_STRING_ROUTINES, KL_IMPORTED_ANY_ROUTINES, UC_IMPORTED_UTF8_ROUTINES, UC_IMPORTED_UTF16_ROUTINES

Creation

Features

Invariants

indexing

description

Variant of KI_CHARACTER_INPUT_STREAM that accepts UTF16 and Latin1 and converts it to UTF8

library

Gobo Eiffel XML Library

copyright

Copyright (c) 2002, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2005/07/13 19:48:54 $

revision

$Revision: 1.12 $

class

XM_EIFFEL_INPUT_STREAM

inherit

KI_CHARACTER_INPUT_STREAM

create

make (a_name: STRING)

-- Create a new stream based on file a_name.

make_from_stream (a_stream: like impl)

-- Create a new stream based on a_stream.

require
a_stream_not_void: a_stream /= Void
ensure
impl_set: impl = a_stream

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 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: unlike the abstract specification, this _often_ but
-- not always returns the same object.)

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

is_applicable_encoding (an_encoding: STRING): BOOLEAN

-- Can the current encoding be switched to an_encoding?

require
valid: is_valid_encoding (an_encoding)
is_valid_encoding (an_encoding: STRING): BOOLEAN

-- Is this encoding known?

set_encoding (an_encoding: STRING)

-- Set encoding.

require
valid_encoding: is_valid_encoding (an_encoding)
applicable_encoding: is_applicable_encoding (an_encoding)

feature -- Input

read_character

-- Read the next item 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_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 (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

last_string: last_string /= Void
impl_not_void: impl /= Void
queue_not_void: utf_queue /= Void

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

end