% $Id: XMLElement.html,v 1.1 2003/10/01 07:22:16 connolly Exp $
%
References
- XML Information Set
Working Draft of August 30, 1999
Editors: John Cowan, David Megginson
XMLElement: trait
includes
XMLInfoSetBasics,
XMLDocument,
XMLEntity,
Set(AttributeItem, FiniteSet[AttributeItem] for Set[E])
% 2.3 Attribute Items
AttributeType enumeration of ID, IDREF, IDREFS, ENTITY,
ENTITIES, NMTOKEN, NMTOKENS, NOTATION,
CDATA, ENUMERATED
introduces
% 2.2. Element Information Items
name: ElementItem → Name
attributes: ElementItem → FiniteSet[AttributeItem] %@@REVIEW: bogus:
% "Namespace declarations are not represented
% as attribute information items."
% check against DOM 1.0 etc.
baseURI: ElementItem → absoluteURI
eStack: List[Item] → List[EntityItem]
externals: List[EntityItem] → List[EntityItem]
% 2.3. Attribute Information Items
name: AttributeItem → Name
specified: AttributeItem → Bool
default: AttributeItem → Value %@@REVIEW default is what?
% sequence of char?
type: AttributeItem → AttributeType
% 2.5. Reference to Skipped Entity Information Items
name: RSEItem → Name
referent: RSEItem → Entity %@@REVIEW: huh? (example/max)
% 2.6. Character Information Items
code: CharacterItem → Int
elementContentWhitespace: CharacterItem → Bool
predefinedEntity: CharacterItem → Bool %@@REVIEW: "included"???
% source
asserts
∀ d: Document,
i, i1, i2: Item,
li, li1, li2: List[Item],
elti: ElementItem,
ei: EntityItem, eli: List[EntityItem],
ai: AttributeItem, sai: FiniteSet[AttributeItem]
% 2.2. Element Information Items
tag(i1) = element
∧ i ∈ children(i1) ⇒ tag(i) = element
∨ tag(i) = pi
∨ tag(i) = rse
∨ tag(i) = comment
∨ tag(i) = entityStart
∨ tag(i) = entityEnd;
% comments, entity start/end markers are optional
tag(i) = element
∧ (i \< descendant \> documentItem(infosetMin(d)))
⇒ len(filter(children(i), comment)) = 0
∧ len(filter(children(i), entityStart)) = 0
∧ len(filter(children(i), entityEnd)) = 0;
% If an entity start marker is present, the
% corresponding entity end marker must also be present ...
tag(i) = element
∧ tag(i1) = entityStart
⇒ entityEnd(end(i1.entityStart)) ∈ children(i);
% ... and vice versa
tag(i) = element
∧ tag(i1) = entityEnd
⇒ entityStart(start(i1.entityEnd)) ∈ children(i);
%@@specify that no two attributes have the same name?
% The absolute URI of the external entity in which
% this element appears.
tag(i) = element
⇒ baseURI(i.element) = systemIdentifier(source(i));
%@@REVIEW: s/absolute URI of external/system identifer of external/
%@@REVIEW: note that this is unspecified in the case of a document
% with no URI, e.g. stdin
% A reference to the entity information item for the entity
% in which this element begins and ends.
% Note we only specify this for the maximal infoset case.@@
i ∈ flatten({documentItem(infosetMax(d))})
∧ children(i) = li1 || {i1} || li2
⇒ source(i1) = (if externals(eStack(li1)) = empty
then source(i)
else head(externals(eStack(li1))));
eStack(empty) = empty;
eStack(li |- i)= (if (tag(i) = entityStart)
then entity(i.entityStart) -| eStack(li)
else if tag(i) = entityEnd
then tail(eStack(li))
else eStack(li));
externals(empty) = empty;
externals(ei -| eli) = (if type(ei).external
then ei -| externals(eli)
else externals(eli));
% 2.3. Attribute Information Items
tag(i1) = attribute
∧ i ∈ children(i1) ⇒ tag(i) = char
∨ tag(i) = entityStart
∨ tag(i) = entityEnd;
% markers are optional
tag(i1) = element
∧ (i1 \< descendant \> documentItem(infosetMin(d)))
∧ tag(i2) = attribute
∧ i2.attribute ∈ attributes(i1.element)
⇒ len(filter(children(i2), entityStart)) = 0
∧ len(filter(children(i2), entityEnd)) = 0;
ai ∈ attributes(elti)
⇒ source(attribute(ai)) = source(element(elti));
[Index]
HTML generated using lsl2html.