% $Id: XMLElement.lsl,v 1.9 2000/01/17 21:33:41 connolly Exp $
%
%html <h2>References</h2>
%html <ol><li><cite><a href="http://www.w3.org/XML/Group/1999/08/WD-xml-infoset-19990830">XML Information Set</a></cite><br />
%html Working Draft of August 30, 1999<br />
%html Editors: John Cowan, David Megginson </ol></li>

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
	\forall 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 \in 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)) \in children(i);
	% ... and vice versa
	tag(i) = element
	/\ tag(i1) = entityEnd
	=> entityStart(start(i1.entityEnd)) \in 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 \in 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 \in 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 \in attributes(i1.element)
	=> len(filter(children(i2), entityStart)) = 0
	   /\ len(filter(children(i2), entityEnd)) = 0;


	ai \in attributes(elti)
	=> source(attribute(ai)) = source(element(elti));