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

kernel.spec.ise

Class KL_CHARACTER_BUFFER


Direct ancestors

KI_CHARACTER_BUFFER, STRING_HANDLER, KL_SHARED_OPERATING_SYSTEM, KL_IMPORTED_ANY_ROUTINES

Creation

Features

Invariants

indexing

description

Character buffers

library

Gobo Eiffel Kernel Library

copyright

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

license

Eiffel Forum License v2 (see forum.txt)

date

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

revision

$Revision: 1.16 $

class

KL_CHARACTER_BUFFER

inherit

KI_CHARACTER_BUFFER
KL_IMPORTED_ANY_ROUTINES

create

make (n: INTEGER)

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

-- (From KI_CHARACTER_BUFFER)

require
non_negative_n: n >= 0
ensure
count_set: count = n
make_from_string (a_string: STRING)

-- Create a new character buffer with
-- characters from a_string.
-- (The newly created buffer and a_string
-- may not share internal representation.)

-- (From KI_CHARACTER_BUFFER)

require
a_string_not_void: a_string /= Void
a_string_is_string: ANY_.same_types (a_string,
)
ensure
count_set: count = a_string.count
charaters_set: to_text.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
string_: KL_STRING_ROUTINES

-- Routines that ought to be in class STRING

-- (From KL_IMPORTED_STRING_ROUTINES)

ensure
string_routines_not_void: Result /= Void
item (i: INTEGER): CHARACTER

-- Item at position i

-- (From KI_BUFFER)

require
i_large_enough: i >= 1
i_small_enough: i <= count
substring (s, e: INTEGER): STRING

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

-- (From KI_CHARACTER_BUFFER)

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

feature -- Measurement

count: INTEGER

-- Number of characters in buffer

-- (From KI_BUFFER)

ensure
count_positive: Result >= 0

feature -- Element change

append_substring_to_string (s, e: INTEGER; a_string: STRING)

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

-- (From KI_CHARACTER_BUFFER)

require
a_string_not_void: a_string /= Void
s_large_enough: s >= 1
e_small_enough: e <= count
valid_interval: s <= e + 1
ensure
count_set: a_string.count = old (a_string.count) + (e - s + 1)
characters_set: s <= e implies STRING_.same_string (a_string.substring (old (a_string.count) + 1, a_string.count), substring (s, e))
fill_from_stream (a_stream: KI_CHARACTER_INPUT_STREAM; pos, nb: INTEGER): INTEGER

-- Fill buffer, starting at position pos, with
-- at most nb characters read from a_stream.
-- Return the number of characters actually read.

-- (From KI_BUFFER)

require
a_stream_not_void: a_stream /= Void
a_stream_open_read: a_stream.is_open_read
not_end_of_input: not a_stream.end_of_input
pos_large_enough: pos >= 1
nb_large_enough: nb > 0
enough_space: (pos + nb - 1) <= count
ensure
nb_item_read_large_enough: Result >= 0
nb_item_read_small_enough: Result <= nb
not_end_of_input: not a_stream.end_of_input implies Result > 0
fill_from_string (a_string: STRING; pos: INTEGER)

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

-- (From KI_CHARACTER_BUFFER)

require
a_string_not_void: a_string /= Void
a_string_is_string: ANY_.same_types (a_string,
)
pos_large_enough: pos >= 1
enough_space: (pos + a_string.count - 1) <= count
ensure
charaters_set: substring (pos, a_string.count + pos - 1).is_equal (a_string)
move_left (old_pos, new_pos: INTEGER; nb: INTEGER)

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

-- (From KI_BUFFER)

require
nb_positive: nb >= 0
old_pos_large_enough: old_pos >= 1
enough_characters: (old_pos + nb - 1) <= count
new_pos_large_enough: new_pos >= 1
enough_space: (new_pos + nb - 1) <= count
move_left: old_pos > new_pos
move_right (old_pos, new_pos: INTEGER; nb: INTEGER)

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

-- (From KI_BUFFER)

require
nb_positive: nb >= 0
old_pos_large_enough: old_pos >= 1
enough_characters: (old_pos + nb - 1) <= count
new_pos_large_enough: new_pos >= 1
enough_space: (new_pos + nb - 1) <= count
move_right: old_pos < new_pos
put (v: CHARACTER; i: INTEGER)

-- Replace character at position i by v.

-- (From KI_BUFFER)

require
i_large_enough: i >= 1
i_small_enough: i <= count
ensure
inserted: item (i) = v

feature -- Resizing

resize (n: INTEGER)

-- Resize buffer so that it contains n characters.
-- Do not lose any previously entered characters.

-- (From KI_BUFFER)

require
n_large_enough: n >= count
ensure
count_set: count = n

feature -- Conversion

as_special: SPECIAL [CHARACTER]

-- 'SPECIAL [CHARACTER]' version of current character buffer;
-- Characters are indexed starting at 1;
-- May return void in some descendants, and the result may share
-- the internal data with Current

-- (From KI_CHARACTER_BUFFER)

to_text: STRING

-- New string made up of characters held in buffer

-- (From KI_CHARACTER_BUFFER)

ensure
to_text_not_void: Result /= Void
string_type: ANY_.same_types (Result,
)
same_count: Result.count = count

invariant

area_not_void: area /= Void

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

end