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

xml.position

Class XM_POSITION_TABLE



Creation

Features

Invariants

indexing

description

Tables which map XML nodes to their positions in source documents

library

Gobo Eiffel XML Library

copyright

Copyright (c) 2001, Andreas Leitner and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2005/07/13 19:49:00 $

revision

$Revision: 1.12 $

class

XM_POSITION_TABLE

create

make

-- Create a new position table.

feature -- Access

item (a_node: XM_NODE): XM_POSITION

-- Position associated with a_node

require
a_node_not_void: a_node /= Void
has_node: has (a_node)
ensure
position_not_void: Result /= Void

feature -- Status report

has (a_node: XM_NODE): BOOLEAN

-- Is there a position associated with a_node?

require
a_node_not_void: a_node /= Void

feature -- Element change

put (a_position: XM_POSITION; a_node: XM_NODE)

-- Associate a_node with position a_position.

require
a_position_not_void: a_position /= Void
a_node_not_void: a_node /= Void
not_has_node: not has (a_node)
ensure
has_node: has (a_node)
inserted: item (a_node) = a_position

invariant

table_not_void: table /= Void
no_void_pair: not table.has (Void)

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

end