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

kernel.spec.ise

Class KL_STRING_BUFFER_ROUTINES


Direct ancestors

KL_IMPORTED_STRING_BUFFER_ROUTINES, KL_IMPORTED_INPUT_STREAM_ROUTINES, KL_IMPORTED_ANY_ROUTINES, STRING_HANDLER

Features

Invariants

indexing

description

Routines that ought to be in a class STRING_BUFFER. %
%A string buffer is a sequence of characters equipped %
%with features put, item and count.

library

Gobo Eiffel Kernel Library

copyright

Copyright (c) 1999-2001, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2005/06/04 20:07:28 $

revision

$Revision: 1.9 $

class

KL_STRING_BUFFER_ROUTINES

obsolete

[020717] Use descendants of KI_CHARACTER_BUFFER instead.

inherit

KL_IMPORTED_STRING_BUFFER_ROUTINES
KL_IMPORTED_INPUT_STREAM_ROUTINES
KL_IMPORTED_ANY_ROUTINES
STRING_HANDLER

feature -- Initialization

make (n: INTEGER): like STRING_BUFFER_TYPE

-- Create a new string buffer being able
-- to contain n characters.

require
non_negative_n: n >= 0
ensure
string_buffer_not_void: Result /= Void
count_set: Result.count = n
make_from_string (a_string: STRING): like STRING_BUFFER_TYPE

-- Create a new string buffer with characters from a_string.

require
a_string_not_void: a_string /= Void
is_string: ANY_.same_types (a_string,
)
ensure
string_buffer_not_void: Result /= Void
count_set: Result.count = a_string.count
charaters_set: substring (Result, lower, a_string.count + lower - 1).is_equal (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
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
string_buffer_: KL_STRING_BUFFER_ROUTINES

-- Routines that ought to be in class STRING_BUFFER

-- (From KL_IMPORTED_STRING_BUFFER_ROUTINES)

ensure
string_buffer_routines_not_void: Result /= Void
substring (a_buffer: like STRING_BUFFER_TYPE; s, e: INTEGER): STRING

-- New string made up of characters held in
-- a_buffer between indexes s and e

require
a_buffer_not_void: a_buffer /= Void
s_large_enough: s >= lower
e_small_enough: e <= upper (a_buffer)
valid_interval: s <= e + 1
ensure
substring_not_void: Result /= Void
is_string: ANY_.same_types (Result,
)
count_set: Result.count = e - s + 1

feature -- Measurement

lower: INTEGER

-- Lower index

upper (a_buffer: like STRING_BUFFER_TYPE): INTEGER

-- Upper index

require
a_buffer_not_void: a_buffer /= Void
ensure
definition: a_buffer.count = (Result - lower + 1)

feature -- Element change

append_substring_to_string (a_buffer: like STRING_BUFFER_TYPE; s, e: INTEGER; a_string: STRING)

-- Append string made up of characters held in a_buffer
-- between indexes s and e to a_string.

require
a_buffer_not_void: a_buffer /= Void
a_string_not_void: a_string /= Void
is_string: ANY_.same_types (a_string,
)
not_same: to_string_buffer (a_string) /= a_buffer
s_large_enough: s >= lower
e_small_enough: e <= upper (a_buffer)
valid_interval: s <= e + 1
ensure
count_set: a_string.count = old (a_string.count) + (e - s + 1)
characters_set: s <= e implies a_string.substring (old (a_string.count) + 1, a_string.count).is_equal (substring (a_buffer, s, e))
copy_from_stream (a_buffer: like STRING_BUFFER_TYPE; pos: INTEGER; a_stream: like INPUT_STREAM_TYPE; 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_buffer_not_void: a_buffer /= Void
pos_large_enough: pos >= lower
a_stream_not_void: a_stream /= Void
a_stream_open_read: INPUT_STREAM_.is_open_read (a_stream)
nb_char_large_enough: nb_char >= 0
enough_space: (pos + nb_char - 1) <= upper (a_buffer)
ensure
nb_char_read_large_enough: Result >= 0
nb_char_read_small_enough: Result <= nb_char
copy_from_string (a_buffer: like STRING_BUFFER_TYPE; pos: INTEGER; a_string: STRING)

-- Copy characters of a_string to a_buffer
-- starting at position pos.

require
a_buffer_not_void: a_buffer /= Void
a_string_not_void: a_string /= Void
is_string: ANY_.same_types (a_string,
)
not_same: to_string_buffer (a_string) /= a_buffer
pos_large_enough: pos >= lower
enough_space: (pos + a_string.count - 1) <= upper (a_buffer)
ensure
charaters_set: substring (a_buffer, pos, a_string.count + pos - 1).is_equal (a_string)
move_left (a_buffer: like STRING_BUFFER_TYPE; old_pos, new_pos: INTEGER; nb: INTEGER)

-- Copy nb characters from old_pos to
-- new_pos in a_buffer.

require
a_buffer_not_void: a_buffer /= Void
nb_positive: nb >= 0
old_pos_large_enough: old_pos >= lower
enough_characters: (old_pos + nb - 1) <= upper (a_buffer)
new_pos_large_enough: new_pos >= lower
enough_space: (new_pos + nb - 1) <= upper (a_buffer)
move_left: old_pos > new_pos
move_right (a_buffer: like STRING_BUFFER_TYPE; old_pos, new_pos: INTEGER; nb: INTEGER)

-- Copy nb characters from old_pos to
-- new_pos in a_buffer.

require
a_buffer_not_void: a_buffer /= Void
nb_positive: nb >= 0
old_pos_large_enough: old_pos >= lower
enough_characters: (old_pos + nb - 1) <= upper (a_buffer)
new_pos_large_enough: new_pos >= lower
enough_space: (new_pos + nb - 1) <= upper (a_buffer)
move_right: old_pos < new_pos

feature -- Resizing

resize (a_buffer: like STRING_BUFFER_TYPE; n: INTEGER): like STRING_BUFFER_TYPE

-- Resize a_buffer so that it contains n characters.
-- Do not lose any previously entered characters.
-- Note: the returned string buffer might be a_buffer or
-- a newly created string buffer where characters from
-- a_buffer have been copied to.

require
a_buffer_not_void: a_buffer /= Void
n_large_enough: n >= a_buffer.count
ensure
string_buffer_not_void: Result /= Void
count_set: Result.count = n

feature -- Conversion

to_string_buffer (a_string: STRING): like STRING_BUFFER_TYPE

-- String buffer filled with characters from a_string.
-- The string buffer and a_string may share internal
-- data. Use make_from_string if this is a concern.

require
a_string_not_void: a_string /= Void
is_string: ANY_.same_types (a_string,
)
ensure
string_buffer_not_void: Result /= Void
count_set: Result.count >= a_string.count
charaters_set: substring (Result, lower, a_string.count + lower - 1).is_equal (a_string)

feature -- Type anchors

invariant


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

end