108 |
|
|
109 |
public Position createPosition(final int offset) throws BadLocationException |
public Position createPosition(final int offset) throws BadLocationException |
110 |
{ |
{ |
111 |
if (offset < 0 || offset > getLength()) |
return content.createPosition(offset); |
|
throw new BadLocationException(getText(0, getLength()), offset); |
|
|
|
|
|
return new Position() |
|
|
{ |
|
|
public int getOffset() |
|
|
{ |
|
|
return offset; |
|
|
} |
|
|
}; |
|
112 |
} |
} |
113 |
|
|
114 |
protected void fireChangedUpdate(DocumentEvent event) |
protected void fireChangedUpdate(DocumentEvent event) |
838 |
public class LeafElement extends AbstractElement |
public class LeafElement extends AbstractElement |
839 |
{ |
{ |
840 |
private static final long serialVersionUID = 5115368706941283802L; |
private static final long serialVersionUID = 5115368706941283802L; |
841 |
int start; |
|
842 |
int end; |
/** Manages the start offset of this element. */ |
843 |
|
Position startPos; |
844 |
|
|
845 |
|
/** Manages the end offset of this element. */ |
846 |
|
Position endPos; |
847 |
|
|
848 |
public LeafElement(Element parent, AttributeSet attributes, int start, |
public LeafElement(Element parent, AttributeSet attributes, int start, |
849 |
int end) |
int end) |
850 |
{ |
{ |
851 |
super(parent, attributes); |
super(parent, attributes); |
852 |
this.start = start; |
try |
853 |
this.end = end; |
{ |
854 |
|
startPos = parent.getDocument().createPosition(start); |
855 |
|
endPos = parent.getDocument().createPosition(end); |
856 |
|
} |
857 |
|
catch (BadLocationException ex) |
858 |
|
{ |
859 |
|
throw new AssertionError("BadLocationException must not be thrown " |
860 |
|
+ "here. start=" + start + ", end=" + end |
861 |
|
+ ", length=" + getLength()); |
862 |
|
} |
863 |
} |
} |
864 |
|
|
865 |
public Enumeration children() |
public Enumeration children() |
889 |
|
|
890 |
public int getEndOffset() |
public int getEndOffset() |
891 |
{ |
{ |
892 |
return end; |
return endPos.getOffset(); |
893 |
} |
} |
894 |
|
|
895 |
public String getName() |
public String getName() |
899 |
|
|
900 |
public int getStartOffset() |
public int getStartOffset() |
901 |
{ |
{ |
902 |
return start; |
return startPos.getOffset(); |
903 |
} |
} |
904 |
|
|
905 |
public boolean isLeaf() |
public boolean isLeaf() |