public class JGlossHTMLDoc extends HTMLDocument
JGloss XML document
.
The JGloss HTML document is generated from the JGloss XML document via a XSLT style sheet.
If the HTML document is changed, the XML document is marked as invalid and is re-generated
from the HTML document via class HTMLToSAXParserAdapter
.
The HTML document is used whenever the document content or structure needs to be changed.
The XML document is used when an external well-defined representation is needed, such as
when saving or exporting the document.Modifier and Type | Class and Description |
---|---|
static interface |
JGlossHTMLDoc.Attributes |
HTMLDocument.BlockElement, HTMLDocument.HTMLReader, HTMLDocument.Iterator, HTMLDocument.RunElement
DefaultStyledDocument.AttributeUndoableEdit, DefaultStyledDocument.ElementBuffer, DefaultStyledDocument.ElementSpec, DefaultStyledDocument.SectionElement
AbstractDocument.AbstractElement, AbstractDocument.AttributeContext, AbstractDocument.BranchElement, AbstractDocument.Content, AbstractDocument.DefaultDocumentEvent, AbstractDocument.ElementEdit, AbstractDocument.LeafElement
Modifier and Type | Field and Description |
---|---|
static String |
EMPTY_ELEMENT_PLACEHOLDER |
AdditionalComments
buffer, BUFFER_SIZE_DEFAULT
BAD_LOCATION, BidiElementName, ContentElementName, ElementNameAttribute, listenerList, ParagraphElementName, SectionElementName
StreamDescriptionProperty, TitleProperty
Modifier and Type | Method and Description |
---|---|
void |
addAnnotation(int start,
int end,
JGlossEditorKit editorKit)
Adds a new annotation for a part of the document.
|
void |
addPropertyChangeListener(PropertyChangeListener listener)
Adds a listener which will be notified of changes to the document title.
|
Element |
getAnnotationElement(int offset)
Returns the annotation element spanning the given element offset.
|
List<Element> |
getAnnotationElements()
Returns a list of all annotation elements.
|
JGlossDocument |
getJGlossDocument() |
Element |
getParagraphElement(int offset) |
int |
getParsePosition()
Returns the position in the document the current reader is at.
|
HTMLEditorKit.ParserCallback |
getReader(int pos)
Returns a reader for a document at the given position.
|
HTMLEditorKit.ParserCallback |
getReader(int pos,
int popDepth,
int pushDepth,
HTML.Tag insertTag)
Returns a reader for a document at the given position.
|
String |
getTitle()
Returns the title of the document.
|
String |
getUnannotatedText(int start,
int end)
Returns only the base text of the selected span, not reading and translation annotations.
|
void |
removeAnnotationElement(Element annotation)
Remove an annotation element.
|
void |
removeAnnotations(int start,
int end)
Remove all annotations which intersect the given region of the document.
|
void |
removePropertyChangeListener(PropertyChangeListener listener)
Removes a previously added document change listener.
|
void |
setAttribute(MutableAttributeSet attr,
Object key,
Object value,
boolean fireChanged)
Sets an attribute to a new value.
|
void |
setJGlossDocument(JGlossDocument _baseDoc)
Set the JGloss XML document to which this HTML document corresponds.
|
void |
setStrictParsing(boolean strict)
Switches strict HTML parsing on or off.
|
void |
setTitle(String title)
Sets the title of the document.
|
create, createBranchElement, createDefaultRoot, createLeafElement, fireChangedUpdate, fireUndoableEditUpdate, getBase, getElement, getElement, getIterator, getParser, getPreservesUnknownTags, getStyleSheet, getTokenThreshold, insert, insertAfterEnd, insertAfterStart, insertBeforeEnd, insertBeforeStart, insertUpdate, processHTMLFrameHyperlinkEvent, setBase, setInnerHTML, setOuterHTML, setParagraphAttributes, setParser, setPreservesUnknownTags, setTokenThreshold
addDocumentListener, addStyle, getBackground, getCharacterElement, getDefaultRootElement, getFont, getForeground, getLogicalStyle, getStyle, getStyleNames, removeDocumentListener, removeElement, removeStyle, removeUpdate, setCharacterAttributes, setLogicalStyle, styleChanged
addUndoableEditListener, createPosition, dump, fireInsertUpdate, fireRemoveUpdate, getAsynchronousLoadPriority, getAttributeContext, getBidiRootElement, getContent, getCurrentWriter, getDocumentFilter, getDocumentListeners, getDocumentProperties, getEndPosition, getLength, getListeners, getProperty, getRootElements, getStartPosition, getText, getText, getUndoableEditListeners, insertString, postRemoveUpdate, putProperty, readLock, readUnlock, remove, removeUndoableEditListener, render, replace, setAsynchronousLoadPriority, setDocumentFilter, setDocumentProperties, writeLock, writeUnlock
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
addUndoableEditListener, createPosition, getEndPosition, getLength, getProperty, getRootElements, getStartPosition, getText, getText, insertString, putProperty, remove, removeUndoableEditListener, render
public static final String EMPTY_ELEMENT_PLACEHOLDER
public void setJGlossDocument(JGlossDocument _baseDoc)
public JGlossDocument getJGlossDocument()
public HTMLEditorKit.ParserCallback getReader(int pos)
JGlossReader
.getReader
in class HTMLDocument
pos
- Position in the document.public HTMLEditorKit.ParserCallback getReader(int pos, int popDepth, int pushDepth, HTML.Tag insertTag)
JGlossReader
.getReader
in class HTMLDocument
pos
- Position in the document.popDepth
- The number of ElementSpec.EndTagTypes to generate before insertingpushDepth
- The number of ElementSpec.StartTagTypes with a direction of
ElementSpec.JoinNextDirection that should be generated before
inserting, but after the end tags have been generated.insertTag
- The first tag to start inserting into document.public int getParsePosition()
public void setAttribute(MutableAttributeSet attr, Object key, Object value, boolean fireChanged)
attr
- The attribute set to change.key
- Key of the attribute.value
- New value of the attribute; or null
to remove the attribute.fireChanged
- true
if a document changed event should be triggered.public void setStrictParsing(boolean strict)
JGlossParser.setStrict(boolean)
public List<Element> getAnnotationElements()
public void addPropertyChangeListener(PropertyChangeListener listener)
public void removePropertyChangeListener(PropertyChangeListener listener)
public void setTitle(String title)
DocumentTitle
property
of the Document object. Calling this method fires a property change event.public String getTitle()
DocumentTitle
property.public String getUnannotatedText(int start, int end)
public Element getParagraphElement(int offset)
getParagraphElement
in interface StyledDocument
getParagraphElement
in class DefaultStyledDocument
public Element getAnnotationElement(int offset)
null
is returned.public void addAnnotation(int start, int end, JGlossEditorKit editorKit)
start
- Start offset of the interval to annotate.end
- End offset of the interval to annotate.editorKit
- Editor kit needed to insert the newly generated annotation element.public void removeAnnotations(int start, int end)
public void removeAnnotationElement(Element annotation)
Copyright © 2001-2013 the JGloss developers. All Rights Reserved.