org.activemath.omdocjdom
Class OJDocument

java.lang.Object
  org.jdom.Document
      org.activemath.omdocjdom.OJDocument

All Implemented Interfaces:

Serializable, Cloneable, org.jdom.Parent

public class OJDocument
extends org.jdom.Document

A generic subclass of Document to provide support for origin tracking (getCollectionID() and getFile().

Version:

See Also:

Serialized Form

Field Summary

protected OJCollection	collection
protected Object	info

Fields inherited from class org.jdom.Document

baseURI

Constructor Summary

OJDocument()
Constructs an OJDocument with an empty omdoc element and a doctype constructed OJConstants.DTD_SYSTEMID.

OJDocument(org.jdom.Element rootElement)
Constructs an OJDocument with arbitrary root and without docType.

OJDocument(org.jdom.Element rootElement, org.jdom.DocType docType)
Constructs an OJDocument with arbitrary root and docType.

OJDocument(org.jdom.Element rootElement, org.jdom.DocType docType, String baseURI)

Method Summary

OJElement	findElementWithID(ID id) A method to find back id-ed elements.
String	getCollectionID()
File	getFile() Get the file mentionned by the setFile(java.io.File) method, or null if none was set.
Object	getInfo()
Date	getLastModificationDate() Returns the the modification date of the file when it was loaded by the setFile(java.io.File) method.
Iterator	listItems()
void	setCollection(OJCollection s) Sets a "collection", whichever that can mean.
void	setFile(File file) Set the file this element was loaded from, if any.
void	setInfo(Object i)
String	toString()
void	writeDocument() Outputs the document to the given file using the UTF-8 encoding.
void	writeDocument(String encoding) Outputs the document to the given file using the given encoding, which supposed to be UTF-8 if none other was given.

Methods inherited from class org.jdom.Document

addContent, addContent, addContent, addContent, clone, cloneContent, detachRootElement, equals, getBaseURI, getContent, getContent, getContent, getContentSize, getDescendants, getDescendants, getDocType, getDocument, getParent, getProperty, getRootElement, hashCode, hasRootElement, indexOf, removeContent, removeContent, removeContent, removeContent, setBaseURI, setContent, setContent, setContent, setContent, setDocType, setProperty, setRootElement

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

collection

protected OJCollection collection

info

protected Object info

Constructor Detail

OJDocument

public OJDocument()

Constructs an OJDocument with an empty omdoc element and a doctype constructed OJConstants.DTD_SYSTEMID.

OJDocument

public OJDocument(org.jdom.Element rootElement,
                  org.jdom.DocType docType)

Constructs an OJDocument with arbitrary root and docType.

OJDocument

public OJDocument(org.jdom.Element rootElement,
                  org.jdom.DocType docType,
                  String baseURI)

OJDocument

public OJDocument(org.jdom.Element rootElement)

Constructs an OJDocument with arbitrary root and without docType.

Method Detail

findElementWithID

public OJElement findElementWithID(ID id)

A method to find back id-ed elements. the current one performs a real search, it may be however, a time where the elements that can be IDs (as of the DTD) and have one ID register themselves so that ID manipulations is much faster.

The current method goes through the whole tree stopping at OMOBJ elements' depth until it finds the given ID. At each node, it requests the ID (using OJElement.getID()) and compares it to this one.

setCollection

public void setCollection(OJCollection s)

Sets a "collection", whichever that can mean. This setting has the equivalent meaning of the ID.getCollection().

getCollectionID

public String getCollectionID()

listItems

public Iterator listItems()

setInfo

public void setInfo(Object i)

getInfo

public Object getInfo()

setFile

public void setFile(File file)

Set the file this element was loaded from, if any. Could turn into an URL one day.

getFile

public File getFile()

Get the file mentionned by the setFile(java.io.File) method, or null if none was set.

getLastModificationDate

public Date getLastModificationDate()

Returns the the modification date of the file when it was loaded by the setFile(java.io.File) method.

writeDocument

public void writeDocument()
                   throws IOException

Outputs the document to the given file using the UTF-8 encoding. Call writeDocument(String).

Throws:

IOException

writeDocument

public void writeDocument(String encoding)
                   throws IOException

Outputs the document to the given file using the given encoding, which supposed to be UTF-8 if none other was given. This is performed after cloning the whole document first (the cloning being synchronized on this object) and removing the "dependency" and "inversed-dependency" of all items.

The output is printed as much as possible by keeping all the formatting of the original source.

Throws:

IOException

toString

public String toString()

Overrides:

toString in class org.jdom.Document