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

xml.tree

Class XM_COMPOSITE


Direct ancestors

XM_NODE, XM_LINKED_LIST, KL_IMPORTED_STRING_ROUTINES

Known direct descendants

XM_ELEMENT, XM_DOCUMENT

Features

Invariants

indexing

description

XML nodes that can contain other xml nodes

library

Gobo Eiffel XML Library

copyright

Copyright (c) 2001, Andreas Leitner and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2005/06/04 22:47:39 $

revision

$Revision: 1.32 $

deferred class

XM_COMPOSITE

inherit

XM_NODE
XM_LINKED_LIST
KL_IMPORTED_STRING_ROUTINES

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
element_by_name (a_name: STRING): XM_ELEMENT

-- Direct child element with name a_name;
-- If there are more than one element with that name, anyone may be returned.
-- Return Void if no element with that name is a child of current node.

require
a_name_not_void: a_name /= Void
ensure
element_not_void: has_element_by_name (a_name) = (Result /= Void)
element_by_qualified_name (a_uri: STRING; a_name: STRING): XM_ELEMENT

-- Direct child element with given qualified name;
-- If there are more than one element with that name, anyone may be returned.
-- Return Void if no element with that name is a child of current node.

require
a_uri_not_void: a_uri /= Void
a_name_not_void: a_name /= Void
ensure
element_not_void: has_element_by_qualified_name (a_uri, a_name) = (Result /= Void)
elements: DS_LIST [XM_ELEMENT]

-- List of all direct child elements in current element
-- (Create a new list at each call.)

ensure
not_void: Result /= Void
equality_tester: KL_EQUALITY_TESTER [XM_NODE]

-- Equality tester;
-- A void equality tester means that =
-- will be used as comparison criterion.

-- (From DS_SEARCHABLE)

first: XM_NODE

-- First item in list
-- (Performance: O(1).)

-- (From DS_LINEAR)

require
not_empty: not is_empty
ensure
has_first: has (Result)
has_element_by_name (a_name: STRING): BOOLEAN

-- Has current node at least one direct child
-- element with the name a_name?

require
a_name_not_void: a_name /= Void
has_element_by_qualified_name (a_uri: STRING; a_name: STRING): BOOLEAN

-- Has current node at least one direct child
-- element with given qualified name ?

require
a_uri_not_void: a_uri /= Void
a_name_not_void: a_name /= Void
index: INTEGER

-- Index of current internal cursor position

-- (From DS_LIST)

ensure
valid_index: valid_index (Result)
infix "@" (i: INTEGER): XM_NODE

-- Item at index i
-- (Performance: O(i).)

-- (From DS_INDEXABLE)

require
valid_index: 1 <= i and i <= count
item (i: INTEGER): XM_NODE

-- Item at index i
-- (Performance: O(i).)

-- (From DS_INDEXABLE)

require
valid_index: 1 <= i and i <= count
item_for_iteration: XM_NODE

-- Item at internal cursor position

-- (From DS_TRAVERSABLE)

require
not_off: not off
last: XM_NODE

-- Last item in list
-- (Performance: O(1).)

-- (From DS_BILINEAR)

require
not_empty: not is_empty
ensure
has_last: has (Result)
new_cursor: DS_LINKED_LIST_CURSOR [XM_NODE]

-- New external cursor for traversal

-- (From DS_TRAVERSABLE)

ensure
cursor_not_void: Result /= Void
valid_cursor: valid_cursor (Result)
parent: XM_COMPOSITE

-- Parent of current node;
-- Void if current node is root

-- (From XM_NODE)

feature -- Measurement

count: INTEGER

-- Number of items in list
-- (Performance: O(1).)

-- (From DS_CONTAINER)

occurrences (v: XM_NODE): INTEGER

-- Number of times v appears in list
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_SEARCHABLE)

ensure
positive: Result >= 0
has: has (v) implies Result >= 1

feature -- Comparison

is_equal (other: like Current): BOOLEAN

-- Is list equal to other?
-- Do not take cursor positions nor
-- equality_tester into account.
-- (Performance: O(count).)

-- (From ANY)

require
other_not_void: other /= Void
ensure
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result

feature -- Status report

after: BOOLEAN

-- Is there no valid position to right of internal cursor?

-- (From DS_LINEAR)

before: BOOLEAN

-- Is there no valid position to left of internal cursor?

-- (From DS_BILINEAR)

equality_tester_settable (a_tester: like equality_tester): BOOLEAN

-- Can set_equality_tester be called with a_tester
-- as argument in current state of container?
-- (Default answer: True.)

-- (From DS_SEARCHABLE)

extendible (n: INTEGER): BOOLEAN

-- May list be extended with n items?

-- (From DS_EXTENDIBLE)

require
positive_n: n >= 0
ensure then
definition: Result = True
has (v: XM_NODE): BOOLEAN

-- Does list include v?
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_SEARCHABLE)

ensure
not_empty: Result implies not is_empty
is_empty: BOOLEAN

-- Is container empty?

-- (From DS_CONTAINER)

is_first: BOOLEAN

-- Is this node the first in its parent's child list,
-- or the root node?

-- (From XM_NODE)

ensure
definition: Result = (is_root_node or else (parent.first = Current))
is_last: BOOLEAN

-- Is this node the last in its parent's child list,
-- or the root node?

-- (From XM_NODE)

ensure
definition: Result = (is_root_node or else (parent.last = Current))
is_root_node: BOOLEAN

-- Is current node the root node?

-- (From XM_NODE)

ensure
definition: Result = (parent = Void)
level: INTEGER

-- Depth at which current node appears relative to its root
-- (The root node has the level 1.)

-- (From XM_NODE)

ensure
root_level: is_root_node implies (Result = 1)
list_is_first: BOOLEAN

-- Is internal cursor on first item?

-- (From DS_LINEAR)

ensure
not_empty: Result implies not is_empty
not_off: Result implies not off
definition: Result implies (item_for_iteration = first)
list_is_last: BOOLEAN

-- Is internal cursor on last item?

-- (From DS_BILINEAR)

ensure
not_empty: Result implies not is_empty
not_off: Result implies not off
definition: Result implies (item_for_iteration = last)
off: BOOLEAN

-- Is there no item at internal cursor position?

-- (From DS_TRAVERSABLE)

parent_element: XM_ELEMENT

-- Parent element.

-- (From XM_NODE)

require
not_root_node: not is_root_node
not_root_element: not parent.is_root_node
ensure
result_not_void: Result /= Void
root_node: XM_DOCUMENT

-- Root node of current node

-- (From XM_NODE)

ensure
result_not_void: Result /= Void
same_equality_tester (other: DS_SEARCHABLE [XM_NODE]): BOOLEAN

-- Does container use the same comparison
-- criterion as other?

-- (From DS_SEARCHABLE)

require
other_not_void: other /= Void
same_items (v, u: XM_NODE): BOOLEAN

-- Are v and u considered equal?
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_SEARCHABLE)

same_position (a_cursor: like new_cursor): BOOLEAN

-- Is internal cursor at same position as a_cursor?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
sorted (a_sorter: DS_SORTER [XM_NODE]): BOOLEAN

-- Is container sorted according to a_sorter's criterion?

-- (From DS_SORTABLE)

require
a_sorter_not_void: a_sorter /= Void
valid_cursor (a_cursor: DS_CURSOR [XM_NODE]): BOOLEAN

-- Is a_cursor a valid cursor?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
valid_index (i: INTEGER): BOOLEAN

-- Is i a valid index value?

-- (From DS_LIST)

ensure
definition: Result = (0 <= i and i <= (count + 1))

feature -- Cursor movement

back

-- Move internal cursor to previous position.

-- (From DS_BILINEAR)

require
not_before: not before
finish

-- Move internal cursor to last position.

-- (From DS_BILINEAR)

ensure
empty_behavior: is_empty implies before
not_empty_behavior: not is_empty implies is_last
forth

-- Move internal cursor to next position.

-- (From DS_LINEAR)

require
not_after: not after
go_after

-- Move internal cursor to after position.

-- (From DS_LINEAR)

ensure
after: after
go_before

-- Move internal cursor to before position.

-- (From DS_BILINEAR)

ensure
before: before
go_i_th (i: INTEGER)

-- Move internal cursor to i-th position.

-- (From DS_LIST)

require
valid_index: valid_index (i)
ensure
moved: index = i
go_to (a_cursor: like new_cursor)

-- Move internal cursor to a_cursor's position.

-- (From DS_TRAVERSABLE)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
ensure
same_position: same_position (a_cursor)
search_back (v: XM_NODE)

-- Move internal cursor to first position at or before current
-- position where item_for_iteration and v are equal.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move before if not found.

-- (From DS_BILINEAR)

require
not_off: not off or before
search_forth (v: XM_NODE)

-- Move internal cursor to first position at or after current
-- position where item_for_iteration and v are equal.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move after if not found.

-- (From DS_LINEAR)

require
not_off: not off or after
start

-- Move internal cursor to first position.

-- (From DS_LINEAR)

ensure
empty_behavior: is_empty implies after
not_empty_behavior: not is_empty implies is_first

feature -- Element change

append (other: DS_LINEAR [XM_NODE]i: INTEGER)

-- append with parent processing.

-- (From DS_INDEXABLE)

require
other_not_void: other /= Void
valid_index: 1 <= i and i <= (count + 1)
ensure
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (item (i) = other.first)
append_first (other: DS_LINEAR [XM_NODE])

-- append_first with parent processing.

-- (From DS_INDEXABLE)

require
other_not_void: other /= Void
ensure
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (first = other.first)
append_last (other: DS_LINEAR [XM_NODE])

-- append_last with parent processing.

-- (From DS_EXTENDIBLE)

require
other_not_void: other /= Void
ensure then
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (item (old count + 1) = other.first)
append_left (other: DS_LINEAR [XM_NODE])

-- Add items of other to left of internal cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.

-- (From DS_LIST)

require
other_not_void: other /= Void
not_before: not before
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (old index) = other.first)
append_left_cursor (other: DS_LINEAR [XM_NODE]a_cursor: like new_cursor)

-- append_left_cursor with parent processing.

-- (From DS_LIST)

require
other_not_void: other /= Void
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_before: not a_cursor.before
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (old (a_cursor.index)) = other.first)
append_right (other: DS_LINEAR [XM_NODE])

-- Add items of other to right of internal cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.

-- (From DS_LIST)

require
other_not_void: other /= Void
not_after: not after
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (index + 1) = other.first)
append_right_cursor (other: DS_LINEAR [XM_NODE]a_cursor: like new_cursor)

-- append_right_cursor with parent processing.

-- (From DS_LIST)

require
other_not_void: other /= Void
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_after: not a_cursor.after
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (a_cursor.index + 1) = other.first)
extend (other: DS_LINEAR [XM_NODE]i: INTEGER)

-- extend with parent processing.

-- (From DS_INDEXABLE)

require
other_not_void: other /= Void
extendible: extendible (other.count)
valid_index: 1 <= i and i <= (count + 1)
ensure
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (item (i) = other.first)
extend_first (other: DS_LINEAR [XM_NODE])

-- extend_first with parent processing.

-- (From DS_INDEXABLE)

require
other_not_void: other /= Void
extendible: extendible (other.count)
ensure
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (first = other.first)
extend_last (other: DS_LINEAR [XM_NODE])

-- extend_last with parent processing.

-- (From DS_EXTENDIBLE)

require
other_not_void: other /= Void
extendible: extendible (other.count)
ensure then
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (item (old count + 1) = other.first)
extend_left (other: DS_LINEAR [XM_NODE])

-- Add items of other to left of internal cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.

-- (From DS_LIST)

require
other_not_void: other /= Void
extendible: extendible (other.count)
not_before: not before
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (old index) = other.first)
extend_left_cursor (other: DS_LINEAR [XM_NODE]a_cursor: like new_cursor)

-- extend_left_cursor with parent processing.

-- (From DS_LIST)

require
other_not_void: other /= Void
extendible: extendible (other.count)
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_before: not a_cursor.before
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (old (a_cursor.index)) = other.first)
extend_right (other: DS_LINEAR [XM_NODE])

-- Add items of other to right of internal cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.

-- (From DS_LIST)

require
other_not_void: other /= Void
extendible: extendible (other.count)
not_after: not after
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (index + 1) = other.first)
extend_right_cursor (other: DS_LINEAR [XM_NODE]a_cursor: like new_cursor)

-- extend_right_cursor with parent processing.

-- (From DS_LIST)

require
other_not_void: other /= Void
extendible: extendible (other.count)
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_after: not a_cursor.after
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (a_cursor.index + 1) = other.first)
force (v: XM_NODEi: INTEGER)

-- force with parent processing.

-- (From DS_INDEXABLE)

require
valid_index: 1 <= i and i <= (count + 1)
ensure
one_more: count = old count + 1
inserted: item (i) = v
force_first (v: XM_NODE)

-- force_first with parent processing.

-- (From DS_INDEXABLE)

ensure
one_more: count = old count + 1
inserted: first = v
force_last (v: XM_NODE)

-- force_last with parent processing.

-- (From DS_EXTENDIBLE)

ensure
added: has (v)
ensure then
one_more: count = old count + 1
inserted: last = v
force_left (v: XM_NODE)

-- Add v to left of internal cursor position.
-- Do not move cursors.

-- (From DS_LIST)

require
not_before: not before
ensure
one_more: count = old count + 1
force_left_cursor (v: XM_NODEa_cursor: like new_cursor)

-- force_left_cursor with parent processing.

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_before: not a_cursor.before
ensure
one_more: count = old count + 1
force_right (v: XM_NODE)

-- Add v to right of internal cursor position.
-- Do not move cursors.

-- (From DS_LIST)

require
not_after: not after
ensure
one_more: count = old count + 1
force_right_cursor (v: XM_NODEa_cursor: like new_cursor)

-- force_right_cursor with parent processing.

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_after: not a_cursor.after
ensure
one_more: count = old count + 1
node_set_parent (a_parent: like parent)

-- Set parent to a_parent.

-- (From XM_NODE)

ensure
parent_set: parent = a_parent
put (v: XM_NODEi: INTEGER)

-- put with parent processing.

-- (From DS_INDEXABLE)

require
extendible: extendible (1)
valid_index: 1 <= i and i <= (count + 1)
ensure
one_more: count = old count + 1
inserted: item (i) = v
put_first (v: XM_NODE)

-- put_first with parent processing.

-- (From DS_INDEXABLE)

require
extendible: extendible (1)
ensure
one_more: count = old count + 1
inserted: first = v
put_last (v: XM_NODE)

-- put_last with parent processing.

-- (From DS_EXTENDIBLE)

require
extendible: extendible (1)
ensure
added: has (v)
ensure then
one_more: count = old count + 1
inserted: last = v
put_left (v: XM_NODE)

-- Add v to left of internal cursor position.
-- Do not move cursors.

-- (From DS_LIST)

require
extendible: extendible (1)
not_before: not before
ensure
one_more: count = old count + 1
put_left_cursor (v: XM_NODEa_cursor: like new_cursor)

-- put_left_cursor with parent processing.

-- (From DS_LIST)

require
extendible: extendible (1)
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_before: not a_cursor.before
ensure
one_more: count = old count + 1
put_right (v: XM_NODE)

-- Add v to right of internal cursor position.
-- Do not move cursors.

-- (From DS_LIST)

require
extendible: extendible (1)
not_after: not after
ensure
one_more: count = old count + 1
put_right_cursor (v: XM_NODEa_cursor: like new_cursor)

-- put_right_cursor with parent processing.

-- (From DS_LIST)

require
extendible: extendible (1)
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_after: not a_cursor.after
ensure
one_more: count = old count + 1
replace (v: XM_NODEi: INTEGER)

-- replace with parent processing.

-- (From DS_INDEXABLE)

require
valid_index: 1 <= i and i <= count
ensure
same_count: count = old count
replaced: item (i) = v
replace_at (v: XM_NODE)

-- replace_at with parent processing.

-- (From DS_LIST)

require
not_off: not off
ensure
same_count: count = old count
replaced: item_for_iteration = v
replace_at_cursor (v: XM_NODEa_cursor: like new_cursor)

-- replace_at_cursor with parent processing.

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_off: not a_cursor.off
ensure
same_count: count = old count
replaced: a_cursor.item = v
set_parent (a_parent: like parent)

-- Set parent to a_parent.

-- (From XM_NODE)

require
a_parent_not_void: a_parent /= Void
not_root_node: not is_root_node
ensure
parent_set: parent = a_parent
swap (i, j: INTEGER)

-- Exchange items at indexes i and j.
-- Do not move cursors.
-- (Performance: O(max(i,j)).)

-- (From DS_INDEXABLE)

require
valid_i: 1 <= i and i <= count
valid_j: 1 <= j and j <= count
ensure
same_count: count = old count
new_i: item (i) = old item (j)
new_j: item (j) = old item (i)

feature -- Removal

delete (v: XM_NODE)

-- Remove all occurrences of v.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move all cursors off.
-- (Performance: O(count).)

-- (From DS_LIST)

ensure
deleted: not has (v)
new_count: count = old (count - occurrences (v))
equality_delete (v: XM_NODE)

-- Delete node if it is in current node, using
-- object identity.

keep_first (n: INTEGER)

-- Keep n first items in list.
-- Move all cursors off.
-- (Performance: O(n).)

-- (From DS_INDEXABLE)

require
valid_n: 0 <= n and n <= count
ensure
new_count: count = n
keep_last (n: INTEGER)

-- Keep n last items in list.
-- Move all cursors off.
-- (Performance: O(count-n).)

-- (From DS_INDEXABLE)

require
valid_n: 0 <= n and n <= count
ensure
new_count: count = n
prune (n: INTEGER; i: INTEGER)

-- Remove n items at and after i-th position.
-- Move all cursors off.
-- (Performance: O(i+n).)

-- (From DS_INDEXABLE)

require
valid_index: 1 <= i and i <= count
valid_n: 0 <= n and n <= (count - i + 1)
ensure
new_count: count = old count - n
prune_first (n: INTEGER)

-- Remove n first items from list.
-- Move all cursors off.
-- (Performance: O(n).)

-- (From DS_INDEXABLE)

require
valid_n: 0 <= n and n <= count
ensure
new_count: count = old count - n
prune_last (n: INTEGER)

-- Remove n last items from list.
-- Move all cursors off.
-- (Performance: O(count-n).)

-- (From DS_INDEXABLE)

require
valid_n: 0 <= n and n <= count
ensure
new_count: count = old count - n
prune_left (n: INTEGER)

-- Remove n items to left of internal cursor position.
-- Move all cursors off.

-- (From DS_LIST)

require
valid_n: 0 <= n and n < index
ensure
new_count: count = old count - n
prune_left_cursor (n: INTEGER; a_cursor: like new_cursor)

-- Remove n items to left of a_cursor position.
-- Move all cursors off.
-- (Synonym of a_cursor.prune_left (n).)
-- (Performance: O(2*a_cursor.index-n).)

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
valid_n: 0 <= n and n < a_cursor.index
ensure
new_count: count = old count - n
prune_right (n: INTEGER)

-- Remove n items to right of internal cursor position.
-- Move all cursors off.

-- (From DS_LIST)

require
valid_n: 0 <= n and n <= (count - index)
ensure
new_count: count = old count - n
prune_right_cursor (n: INTEGER; a_cursor: like new_cursor)

-- Remove n items to right of a_cursor position.
-- Move all cursors off.
-- (Synonym of a_cursor.prune_right (n).)
-- (Performance: O(n).)

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
valid_n: 0 <= n and n <= (count - a_cursor.index)
ensure
new_count: count = old count - n
remove (i: INTEGER)

-- Remove item at i-th position.
-- Move any cursors at this position forth.
-- (Performance: O(i).)

-- (From DS_INDEXABLE)

require
not_empty: not is_empty
valid_index: 1 <= i and i <= count
ensure
one_less: count = old count - 1
remove_at

-- Remove item at internal cursor position.
-- Move any cursors at this position forth.

-- (From DS_LIST)

require
not_off: not off
ensure
one_less: count = old count - 1
remove_at_cursor (a_cursor: like new_cursor)

-- Remove item at a_cursor position.
-- Move any cursors at this position forth.
-- (Synonym of a_cursor.remove.)
-- (Performance: O(count) if a_cursor.is_last, O(1) otherwise.)

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_off: not a_cursor.off
ensure
one_less: count = old count - 1
remove_first

-- Remove item at beginning of list.
-- Move any cursors at this position forth.
-- (Performance: O(1).)

-- (From DS_INDEXABLE)

require
not_empty: not is_empty
ensure
one_less: count = old count - 1
remove_last

-- Remove item at end of list.
-- Move any cursors at this position forth.
-- (Performance: O(count).)

-- (From DS_INDEXABLE)

require
not_empty: not is_empty
ensure
one_less: count = old count - 1
remove_left

-- Remove item to left of internal cursor position.
-- Move any cursors at this position forth.

-- (From DS_LIST)

require
not_empty: not is_empty
not_before: not before
not_first: not is_first
ensure
one_less: count = old count - 1
remove_left_cursor (a_cursor: like new_cursor)

-- Remove item to left of a_cusor position.
-- Move any cursors at this position forth.
-- (Synonym of a_cursor.remove_left.)
-- (Performance: O(a_cursor.index).)

-- (From DS_LIST)

require
not_empty: not is_empty
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_before: not a_cursor.before
not_first: not a_cursor.is_first
ensure
one_less: count = old count - 1
remove_right

-- Remove item to right of internal cursor position.
-- Move any cursors at this position forth.

-- (From DS_LIST)

require
not_empty: not is_empty
not_after: not after
not_last: not is_last
ensure
one_less: count = old count - 1
remove_right_cursor (a_cursor: like new_cursor)

-- Remove item to right of a_cursor position.
-- Move any cursors at this position forth.
-- (Synonym of a_cursor.remove_right.)
-- (Performance: O(1).)

-- (From DS_LIST)

require
not_empty: not is_empty
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_after: not a_cursor.after
not_last: not a_cursor.is_last
ensure
one_less: count = old count - 1
wipe_out

-- Remove all items from list.
-- Move all cursors off.
-- (Performance: O(1).)

-- (From DS_CONTAINER)

ensure
wiped_out: is_empty

feature -- Duplication

cloned_object: like Current

-- Clone of current object

-- (From KL_CLONABLE)

ensure
cloned_not_void: Result /= Void
same_type: ANY_.same_types (Result, Current)
is_equal: Result.is_equal (Current)
copy (other: like Current)

-- Copy other to current list.
-- Move all cursors off (unless other = Current).
-- (Performance: O(other.count).)

-- (From ANY)

require
other_not_void: other /= Void
type_identity: same_type (other)
ensure
is_equal: is_equal (other)
to_array: ARRAY [XM_NODE]

-- Array containing the same items as current
-- container in the same order

-- (From DS_LINEAR)

ensure
to_array_not_void: Result /= Void
same_count: Result.count = count

feature -- Text

join_text_nodes

-- Join sequences of text nodes.

text: STRING

-- Concatenation of all texts directly found in
-- current element; Void if no text found
-- (Return a new string at each call.)

feature -- Processing

process (a_processor: XM_NODE_PROCESSOR)

-- Process current node with a_processor.

-- (From XM_NODE)

require
a_processor_not_void: a_processor /= Void
process_children (a_processor: XM_NODE_PROCESSOR)

-- Process direct children.

require
a_processor_not_void: a_processor /= Void
process_children_recursive (a_processor: XM_NODE_PROCESSOR)

-- Process direct and indirect children.

require
processor_not_void: a_processor /= Void

feature {DS_CURSOR} -- Cursor implementation

add_traversing_cursor (a_cursor: like new_cursor)

-- Add a_cursor to the list of traversing cursors
-- (i.e. cursors associated with current container
-- and which are not currently off).

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
cursor_after (a_cursor: like new_cursor): BOOLEAN

-- Is there no valid position to right of a_cursor?

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
cursor_back (a_cursor: like new_cursor)

-- Move a_cursor to previous position.
-- (Performance: O(a_cursor.index).)

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_before: not cursor_before (a_cursor)
cursor_before (a_cursor: like new_cursor): BOOLEAN

-- Is there no valid position to left of a_cursor?

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
cursor_finish (a_cursor: like new_cursor)

-- Move a_cursor to last position.
-- (Performance: O(1).)

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
empty_behavior: is_empty implies cursor_before (a_cursor)
not_empty_behavior: not is_empty implies cursor_is_last (a_cursor)
cursor_forth (a_cursor: like new_cursor)

-- Move a_cursor to next position.
-- (Performance: O(1).)

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_after: not cursor_after (a_cursor)
cursor_go_after (a_cursor: like new_cursor)

-- Move a_cursor to after position.
-- (Performance: O(1).)

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
a_cursor_after: cursor_after (a_cursor)
cursor_go_before (a_cursor: like new_cursor)

-- Move a_cursor to before position.
-- (Performance: O(1).)

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
a_cursor_before: cursor_before (a_cursor)
cursor_go_i_th (a_cursor: like new_cursor; i: INTEGER)

-- Move a_cursor to i-th position.
-- (Performance: O(i).)

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
valid_index: valid_index (i)
ensure
moved: cursor_index (a_cursor) = i
cursor_go_to (a_cursor, other: like new_cursor)

-- Move a_cursor to other's position.
-- (Performance: O(1).)

-- (From DS_TRAVERSABLE)

require
cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
other_not_void: other /= Void
other_valid: valid_cursor (other)
ensure
same_position: cursor_same_position (a_cursor, other)
cursor_index (a_cursor: like new_cursor): INTEGER

-- Index of a_cursor's current position
-- (Performance: O(count).)

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
valid_index: valid_index (Result)
cursor_is_first (a_cursor: like new_cursor): BOOLEAN

-- Is a_cursor on first item?

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
not_empty: Result implies not is_empty
a_cursor_not_off: Result implies not cursor_off (a_cursor)
definition: Result implies (cursor_item (a_cursor) = first)
cursor_is_last (a_cursor: like new_cursor): BOOLEAN

-- Is a_cursor on last item?

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
not_empty: Result implies not is_empty
a_cursor_not_off: Result implies not cursor_off (a_cursor)
definition: Result implies (cursor_item (a_cursor) = last)
cursor_item (a_cursor: like new_cursor): XM_NODE

-- Item at a_cursor position
-- (Performance: O(1).)

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_off: not cursor_off (a_cursor)
cursor_off (a_cursor: like new_cursor): BOOLEAN

-- Is there no item at a_cursor position?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
cursor_same_position (a_cursor, other: like new_cursor): BOOLEAN

-- Is a_cursor at same position as other?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
other_not_void: other /= Void
cursor_search_back (a_cursor: like new_cursorv: XM_NODE)

-- Move a_cursor to first position at or before its current
-- position where cursor_item (a_cursor) and v are equal.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move before if not found.
-- (Performance: O(a_cursor.index).)

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_off: not cursor_off (a_cursor) or cursor_before (a_cursor)
cursor_search_forth (a_cursor: like new_cursorv: XM_NODE)

-- Move a_cursor to first position at or after its current
-- position where cursor_item (a_cursor) and v are equal.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move after if not found.

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_off: not cursor_off (a_cursor) or cursor_after (a_cursor)
cursor_start (a_cursor: like new_cursor)

-- Move a_cursor to first position.
-- (Performance: O(1).)

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
empty_behavior: is_empty implies cursor_after (a_cursor)
not_empty_behavior: not is_empty implies cursor_is_first (a_cursor)
remove_traversing_cursor (a_cursor: like new_cursor)

-- Remove a_cursor from the list of traversing cursors
-- (i.e. cursors associated with current container
-- and which are not currently off).

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void

feature -- Sort

sort (a_sorter: DS_SORTER [XM_NODE])

-- Sort container using a_sorter's algorithm.

-- (From DS_SORTABLE)

require
a_sorter_not_void: a_sorter /= Void
ensure
sorted: sorted (a_sorter)

feature -- Setting

set_equality_tester (a_tester: like equality_tester)

-- Set equality_tester to a_tester.
-- A void equality tester means that =
-- will be used as comparison criterion.

-- (From DS_SEARCHABLE)

require
equality_tester_settable: equality_tester_settable (a_tester)
ensure
equality_tester_set: equality_tester = a_tester

feature {DS_LINKED_LIST, DS_LINKED_LIST_CURSOR} -- Implementation

first_cell: DS_LINKABLE [XM_NODE]

-- First cell in list

-- (From DS_LINKED_LIST)

last_cell: like first_cell

-- Last cell in list

-- (From DS_LINKED_LIST)

invariant


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

first_cell: is_empty = (first_cell = Void)
last_cell: is_empty = (last_cell = Void)
last_constraint: last_cell /= Void implies last_cell.right = Void

-- From DS_BILINEAR
not_both: initialized implies (not (after and before))
before_constraint: initialized implies (before implies off)

-- From DS_LINEAR
after_constraint: initialized implies (after implies off)

empty_constraint: initialized implies (is_empty implies off)
internal_cursor_not_void: initialized implies (internal_cursor /= Void)
valid_internal_cursor: initialized implies valid_cursor (internal_cursor)

-- From DS_CONTAINER
positive_count: count >= 0
empty_definition: is_empty = (count = 0)

end