41 |
import java.awt.Color; |
import java.awt.Color; |
42 |
import java.awt.Font; |
import java.awt.Font; |
43 |
import java.io.Serializable; |
import java.io.Serializable; |
44 |
|
import java.util.Enumeration; |
45 |
|
import java.util.Stack; |
46 |
import java.util.Vector; |
import java.util.Vector; |
47 |
|
|
48 |
|
import javax.swing.event.ChangeEvent; |
49 |
|
import javax.swing.event.ChangeListener; |
50 |
import javax.swing.event.DocumentEvent; |
import javax.swing.event.DocumentEvent; |
51 |
|
import javax.swing.undo.AbstractUndoableEdit; |
52 |
|
import javax.swing.undo.UndoableEdit; |
53 |
|
|
54 |
/** |
/** |
55 |
* The default implementation of {@link StyledDocument}. |
* The default implementation of {@link StyledDocument}. |
67 |
implements StyledDocument |
implements StyledDocument |
68 |
{ |
{ |
69 |
/** |
/** |
70 |
|
* An {@link UndoableEdit} that can undo attribute changes to an element. |
71 |
|
* |
72 |
|
* @author Roman Kennke (kennke@aicas.com) |
73 |
|
*/ |
74 |
|
public static class AttributeUndoableEdit |
75 |
|
extends AbstractUndoableEdit |
76 |
|
{ |
77 |
|
/** |
78 |
|
* A copy of the old attributes. |
79 |
|
*/ |
80 |
|
protected AttributeSet copy; |
81 |
|
|
82 |
|
/** |
83 |
|
* The new attributes. |
84 |
|
*/ |
85 |
|
protected AttributeSet newAttributes; |
86 |
|
|
87 |
|
/** |
88 |
|
* If the new attributes replaced the old attributes or if they only were |
89 |
|
* added to them. |
90 |
|
*/ |
91 |
|
protected boolean isReplacing; |
92 |
|
|
93 |
|
/** |
94 |
|
* The element that has changed. |
95 |
|
*/ |
96 |
|
protected Element element; |
97 |
|
|
98 |
|
/** |
99 |
|
* Creates a new <code>AttributeUndoableEdit</code>. |
100 |
|
* |
101 |
|
* @param el the element that changes attributes |
102 |
|
* @param newAtts the new attributes |
103 |
|
* @param replacing if the new attributes replace the old or only append to |
104 |
|
* them |
105 |
|
*/ |
106 |
|
public AttributeUndoableEdit(Element el, AttributeSet newAtts, |
107 |
|
boolean replacing) |
108 |
|
{ |
109 |
|
element = el; |
110 |
|
newAttributes = newAtts; |
111 |
|
isReplacing = replacing; |
112 |
|
copy = el.getAttributes().copyAttributes(); |
113 |
|
} |
114 |
|
|
115 |
|
/** |
116 |
|
* Undos the attribute change. The <code>copy</code> field is set as |
117 |
|
* attributes on <code>element</code>. |
118 |
|
*/ |
119 |
|
public void undo() |
120 |
|
{ |
121 |
|
super.undo(); |
122 |
|
AttributeSet atts = element.getAttributes(); |
123 |
|
if (atts instanceof MutableAttributeSet) |
124 |
|
{ |
125 |
|
MutableAttributeSet mutable = (MutableAttributeSet) atts; |
126 |
|
mutable.removeAttributes(atts); |
127 |
|
mutable.addAttributes(copy); |
128 |
|
} |
129 |
|
} |
130 |
|
|
131 |
|
/** |
132 |
|
* Redos an attribute change. This adds <code>newAttributes</code> to the |
133 |
|
* <code>element</code>'s attribute set, possibly clearing all attributes |
134 |
|
* if <code>isReplacing</code> is true. |
135 |
|
*/ |
136 |
|
public void redo() |
137 |
|
{ |
138 |
|
super.undo(); |
139 |
|
AttributeSet atts = element.getAttributes(); |
140 |
|
if (atts instanceof MutableAttributeSet) |
141 |
|
{ |
142 |
|
MutableAttributeSet mutable = (MutableAttributeSet) atts; |
143 |
|
if (isReplacing) |
144 |
|
mutable.removeAttributes(atts); |
145 |
|
mutable.addAttributes(newAttributes); |
146 |
|
} |
147 |
|
} |
148 |
|
} |
149 |
|
|
150 |
|
/** |
151 |
* Carries specification information for new {@link Element}s that should |
* Carries specification information for new {@link Element}s that should |
152 |
* be created in {@link ElementBuffer}. This allows the parsing process |
* be created in {@link ElementBuffer}. This allows the parsing process |
153 |
* to be decoupled from the <code>Element</code> creation process. |
* to be decoupled from the <code>Element</code> creation process. |
430 |
private int length; |
private int length; |
431 |
|
|
432 |
/** |
/** |
433 |
|
* The number of inserted end tags. This is a counter which always gets |
434 |
|
* incremented when an end tag is inserted. This is evaluated before |
435 |
|
* content insertion to go up the element stack. |
436 |
|
*/ |
437 |
|
private int numEndTags; |
438 |
|
|
439 |
|
/** |
440 |
|
* The number of inserted start tags. This is a counter which always gets |
441 |
|
* incremented when an end tag is inserted. This is evaluated before |
442 |
|
* content insertion to go up the element stack. |
443 |
|
*/ |
444 |
|
private int numStartTags; |
445 |
|
|
446 |
|
/** |
447 |
|
* The current position in the element tree. This is used for bulk inserts |
448 |
|
* using ElementSpecs. |
449 |
|
*/ |
450 |
|
private Stack elementStack; |
451 |
|
|
452 |
|
/** |
453 |
* Holds fractured elements during insertion of end and start tags. |
* Holds fractured elements during insertion of end and start tags. |
454 |
* Inserting an end tag may lead to fracturing of the current paragraph |
* Inserting an end tag may lead to fracturing of the current paragraph |
455 |
* element. The elements that have been cut off may be added to the |
* element. The elements that have been cut off may be added to the |
471 |
public ElementBuffer(Element root) |
public ElementBuffer(Element root) |
472 |
{ |
{ |
473 |
this.root = root; |
this.root = root; |
474 |
|
elementStack = new Stack(); |
475 |
} |
} |
476 |
|
|
477 |
/** |
/** |
515 |
{ |
{ |
516 |
// Split up the element at the start offset if necessary. |
// Split up the element at the start offset if necessary. |
517 |
Element el = getCharacterElement(offset); |
Element el = getCharacterElement(offset); |
518 |
split(el, offset); |
Element[] res = split(el, offset, 0); |
519 |
|
BranchElement par = (BranchElement) el.getParentElement(); |
520 |
|
if (res[1] != null) |
521 |
|
{ |
522 |
|
int index = par.getElementIndex(offset); |
523 |
|
Element[] removed; |
524 |
|
Element[] added; |
525 |
|
if (res[0] == null) |
526 |
|
{ |
527 |
|
removed = new Element[0]; |
528 |
|
added = new Element[]{ res[1] }; |
529 |
|
index++; |
530 |
|
} |
531 |
|
else |
532 |
|
{ |
533 |
|
removed = new Element[]{ el }; |
534 |
|
added = new Element[]{ res[0], res[1] }; |
535 |
|
} |
536 |
|
par.replace(index, removed.length, added); |
537 |
|
addEdit(par, index, removed, added); |
538 |
|
} |
539 |
|
|
540 |
int endOffset = offset + length; |
int endOffset = offset + length; |
541 |
el = getCharacterElement(endOffset); |
el = getCharacterElement(endOffset); |
542 |
split(el, endOffset); |
res = split(el, endOffset, 0); |
543 |
|
par = (BranchElement) el.getParentElement(); |
544 |
|
if (res[1] != null) |
545 |
|
{ |
546 |
|
int index = par.getElementIndex(offset); |
547 |
|
Element[] removed; |
548 |
|
Element[] added; |
549 |
|
if (res[1] == null) |
550 |
|
{ |
551 |
|
removed = new Element[0]; |
552 |
|
added = new Element[]{ res[1] }; |
553 |
|
} |
554 |
|
else |
555 |
|
{ |
556 |
|
removed = new Element[]{ el }; |
557 |
|
added = new Element[]{ res[0], res[1] }; |
558 |
|
} |
559 |
|
par.replace(index, removed.length, added); |
560 |
|
addEdit(par, index, removed, added); |
561 |
|
} |
562 |
} |
} |
563 |
|
|
564 |
/** |
/** |
566 |
* |
* |
567 |
* @param el the Element to possibly split |
* @param el the Element to possibly split |
568 |
* @param offset the offset at which to possibly split |
* @param offset the offset at which to possibly split |
569 |
*/ |
* @param space the amount of space to create between the splitted parts |
570 |
void split(Element el, int offset) |
* |
571 |
{ |
* @return An array of elements which represent the split result. This |
572 |
if (el instanceof AbstractElement) |
* array has two elements, the two parts of the split. The first |
573 |
{ |
* element might be null, which means that the element which should |
574 |
AbstractElement ael = (AbstractElement) el; |
* be splitted can remain in place. The second element might also |
575 |
int startOffset = ael.getStartOffset(); |
* be null, which means that the offset is already at an element |
576 |
int endOffset = ael.getEndOffset(); |
* boundary and the element doesn't need to be splitted. |
577 |
int len = endOffset - startOffset; |
* |
578 |
if (startOffset != offset && endOffset != offset) |
*/ |
579 |
{ |
private Element[] split(Element el, int offset, int space) |
580 |
Element paragraph = ael.getParentElement(); |
{ |
581 |
if (paragraph instanceof BranchElement) |
// If we are at an element boundary, then return an empty array. |
582 |
{ |
if ((offset == el.getStartOffset() || offset == el.getEndOffset()) |
583 |
BranchElement par = (BranchElement) paragraph; |
&& space == 0 && el.isLeaf()) |
584 |
Element child1 = createLeafElement(par, ael, startOffset, |
return new Element[2]; |
585 |
offset); |
|
586 |
Element child2 = createLeafElement(par, ael, offset, |
// If the element is an instance of BranchElement, then we recursivly |
587 |
endOffset); |
// call this method to perform the split. |
588 |
int index = par.getElementIndex(startOffset); |
Element[] res = new Element[2]; |
589 |
Element[] add = new Element[]{ child1, child2 }; |
if (el instanceof BranchElement) |
590 |
par.replace(index, 1, add); |
{ |
591 |
documentEvent.addEdit(new ElementEdit(par, index, |
int index = el.getElementIndex(offset); |
592 |
new Element[]{ el }, |
Element child = el.getElement(index); |
593 |
add)); |
Element[] result = split(child, offset, space); |
594 |
} |
Element[] removed; |
595 |
|
Element[] added; |
596 |
|
Element[] newAdded; |
597 |
|
|
598 |
|
int count = el.getElementCount(); |
599 |
|
if (!(result[1] == null)) |
600 |
|
{ |
601 |
|
// This is the case when we can keep the first element. |
602 |
|
if (result[0] == null) |
603 |
|
{ |
604 |
|
removed = new Element[count - index - 1]; |
605 |
|
newAdded = new Element[count - index - 1]; |
606 |
|
added = new Element[]{}; |
607 |
|
} |
608 |
|
// This is the case when we may not keep the first element. |
609 |
else |
else |
610 |
throw new AssertionError("paragraph elements are expected to " |
{ |
611 |
+ "be instances of " |
removed = new Element[count - index]; |
612 |
+ "javax.swing.text.AbstractDocument.BranchElement"); |
newAdded = new Element[count - index]; |
613 |
} |
added = new Element[]{result[0]}; |
614 |
} |
} |
615 |
else |
newAdded[0] = result[1]; |
616 |
throw new AssertionError("content elements are expected to be " |
for (int i = index; i < count; i++) |
617 |
+ "instances of " |
{ |
618 |
+ "javax.swing.text.AbstractDocument.AbstractElement"); |
Element el2 = el.getElement(i); |
619 |
|
int ind = i - count + removed.length; |
620 |
|
removed[ind] = el2; |
621 |
|
if (ind != 0) |
622 |
|
newAdded[ind] = el2; |
623 |
|
} |
624 |
|
|
625 |
|
((BranchElement) el).replace(index, removed.length, added); |
626 |
|
addEdit(el, index, removed, added); |
627 |
|
BranchElement newPar = |
628 |
|
(BranchElement) createBranchElement(el.getParentElement(), |
629 |
|
el.getAttributes()); |
630 |
|
newPar.replace(0, 0, newAdded); |
631 |
|
res = new Element[]{ null, newPar }; |
632 |
|
} |
633 |
|
else |
634 |
|
{ |
635 |
|
removed = new Element[count - index]; |
636 |
|
for (int i = index; i < count; ++i) |
637 |
|
removed[i - index] = el.getElement(i); |
638 |
|
added = new Element[0]; |
639 |
|
((BranchElement) el).replace(index, removed.length, |
640 |
|
added); |
641 |
|
addEdit(el, index, removed, added); |
642 |
|
BranchElement newPar = |
643 |
|
(BranchElement) createBranchElement(el.getParentElement(), |
644 |
|
el.getAttributes()); |
645 |
|
newPar.replace(0, 0, removed); |
646 |
|
res = new Element[]{ null, newPar }; |
647 |
|
} |
648 |
|
} |
649 |
|
else if (el instanceof LeafElement) |
650 |
|
{ |
651 |
|
BranchElement par = (BranchElement) el.getParentElement(); |
652 |
|
Element el1 = createLeafElement(par, el.getAttributes(), |
653 |
|
el.getStartOffset(), offset); |
654 |
|
Element el2 = createLeafElement(par, el.getAttributes(), |
655 |
|
offset + space, el.getEndOffset()); |
656 |
|
res = new Element[]{ el1, el2 }; |
657 |
|
} |
658 |
|
return res; |
659 |
} |
} |
660 |
|
|
661 |
/** |
/** |
678 |
this.offset = offset; |
this.offset = offset; |
679 |
this.length = length; |
this.length = length; |
680 |
documentEvent = ev; |
documentEvent = ev; |
681 |
|
// Push the root and the paragraph at offset onto the element stack. |
682 |
|
elementStack.clear(); |
683 |
|
elementStack.push(root); |
684 |
|
elementStack.push(root.getElement(root.getElementIndex(offset))); |
685 |
|
numEndTags = 0; |
686 |
|
numStartTags = 0; |
687 |
insertUpdate(data); |
insertUpdate(data); |
688 |
} |
} |
689 |
|
|
702 |
switch (data[i].getType()) |
switch (data[i].getType()) |
703 |
{ |
{ |
704 |
case ElementSpec.StartTagType: |
case ElementSpec.StartTagType: |
705 |
insertStartTag(data[i]); |
numStartTags++; |
706 |
break; |
break; |
707 |
case ElementSpec.EndTagType: |
case ElementSpec.EndTagType: |
708 |
insertEndTag(data[i]); |
numEndTags++; |
709 |
break; |
break; |
710 |
default: |
default: |
711 |
insertContentTag(data[i]); |
insertContentTag(data[i]); |
712 |
break; |
break; |
713 |
} |
} |
714 |
} |
} |
715 |
|
endEdit(); |
716 |
} |
} |
717 |
|
|
718 |
/** |
/** |
719 |
* Insert a new paragraph after the paragraph at the current position. |
* Finishes an insertion by possibly evaluating the outstanding start and |
720 |
* |
* end tags. However, this is only performed if the event has received any |
721 |
* @param tag the element spec that describes the element to be inserted |
* modifications. |
722 |
*/ |
*/ |
723 |
void insertStartTag(ElementSpec tag) |
private void endEdit() |
724 |
{ |
{ |
725 |
BranchElement root = (BranchElement) getDefaultRootElement(); |
if (documentEvent.modified) |
726 |
int index = root.getElementIndex(offset); |
prepareContentInsertion(); |
727 |
if (index == -1) |
} |
|
index = 0; |
|
|
|
|
|
BranchElement newParagraph = |
|
|
(BranchElement) createBranchElement(root, tag.getAttributes()); |
|
|
newParagraph.setResolveParent(getStyle(StyleContext.DEFAULT_STYLE)); |
|
|
|
|
|
// Add new paragraph into document structure. |
|
|
Element[] added = new Element[]{newParagraph}; |
|
|
root.replace(index + 1, 0, added); |
|
|
ElementEdit edit = new ElementEdit(root, index + 1, new Element[0], |
|
|
added); |
|
|
documentEvent.addEdit(edit); |
|
728 |
|
|
729 |
// Maybe add fractured elements. |
/** |
730 |
if (tag.getDirection() == ElementSpec.JoinFractureDirection) |
* Evaluates the number of inserted end tags and performs the corresponding |
731 |
|
* structural changes. |
732 |
|
*/ |
733 |
|
private void prepareContentInsertion() |
734 |
|
{ |
735 |
|
while (numEndTags > 0) |
736 |
{ |
{ |
737 |
Element[] newFracture = new Element[fracture.length]; |
elementStack.pop(); |
738 |
for (int i = 0; i < fracture.length; i++) |
numEndTags--; |
739 |
{ |
} |
740 |
Element oldLeaf = fracture[i]; |
|
741 |
Element newLeaf = createLeafElement(newParagraph, |
while (numStartTags > 0) |
742 |
oldLeaf.getAttributes(), |
{ |
743 |
oldLeaf.getStartOffset(), |
Element current = (Element) elementStack.peek(); |
744 |
oldLeaf.getEndOffset()); |
Element newParagraph = |
745 |
newFracture[i] = newLeaf; |
insertParagraph((BranchElement) current, offset); |
746 |
} |
elementStack.push(newParagraph); |
747 |
newParagraph.replace(0, 0, newFracture); |
numStartTags--; |
|
edit = new ElementEdit(newParagraph, 0, new Element[0], |
|
|
fracture); |
|
|
documentEvent.addEdit(edit); |
|
|
fracture = new Element[0]; |
|
748 |
} |
} |
749 |
} |
} |
750 |
|
|
751 |
/** |
private Element insertParagraph(BranchElement par, int offset) |
752 |
* Inserts an end tag into the document structure. This cuts of the |
{ |
753 |
* current paragraph element, possibly fracturing it's child elements. |
Element current = par.getElement(par.getElementIndex(offset)); |
754 |
* The fractured elements are saved so that they can be joined later |
Element[] res = split(current, offset, 0); |
755 |
* with a new paragraph element. |
int index = par.getElementIndex(offset); |
756 |
*/ |
Element ret; |
757 |
void insertEndTag(ElementSpec tag) |
if (res[1] != null) |
758 |
{ |
{ |
759 |
BranchElement root = (BranchElement) getDefaultRootElement(); |
Element[] removed; |
760 |
int parIndex = root.getElementIndex(offset); |
Element[] added; |
761 |
BranchElement paragraph = (BranchElement) root.getElement(parIndex); |
if (res[0] == null) |
762 |
|
{ |
763 |
int index = paragraph.getElementIndex(offset); |
removed = new Element[0]; |
764 |
LeafElement content = (LeafElement) paragraph.getElement(index); |
if (res[1] instanceof BranchElement) |
765 |
// We might have to split the element at offset. |
{ |
766 |
split(content, offset); |
added = new Element[]{ res[1] }; |
767 |
index = paragraph.getElementIndex(offset); |
ret = res[1]; |
768 |
|
} |
769 |
int count = paragraph.getElementCount(); |
else |
770 |
// Store fractured elements. |
{ |
771 |
fracture = new Element[count - index]; |
ret = createBranchElement(par, null); |
772 |
for (int i = index; i < count; ++i) |
added = new Element[]{ ret, res[1] }; |
773 |
fracture[i - index] = paragraph.getElement(i); |
} |
774 |
|
index++; |
775 |
// Delete fractured elements. |
} |
776 |
paragraph.replace(index, count - index, new Element[0]); |
else |
777 |
|
{ |
778 |
// Add this action to the document event. |
removed = new Element[]{ current }; |
779 |
ElementEdit edit = new ElementEdit(paragraph, index, fracture, |
if (res[1] instanceof BranchElement) |
780 |
new Element[0]); |
{ |
781 |
documentEvent.addEdit(edit); |
ret = res[1]; |
782 |
|
added = new Element[]{ res[0], res[1] }; |
783 |
|
} |
784 |
|
else |
785 |
|
{ |
786 |
|
ret = createBranchElement(par, null); |
787 |
|
added = new Element[]{ res[0], ret, res[1] }; |
788 |
|
} |
789 |
|
} |
790 |
|
par.replace(index, removed.length, added); |
791 |
|
addEdit(par, index, removed, added); |
792 |
|
} |
793 |
|
else |
794 |
|
{ |
795 |
|
ret = createBranchElement(par, null); |
796 |
|
Element[] added = new Element[]{ ret }; |
797 |
|
par.replace(index, 0, added); |
798 |
|
addEdit(par, index, new Element[0], added); |
799 |
|
} |
800 |
|
return ret; |
801 |
} |
} |
802 |
|
|
803 |
/** |
/** |
805 |
* |
* |
806 |
* @param tag the element spec |
* @param tag the element spec |
807 |
*/ |
*/ |
808 |
void insertContentTag(ElementSpec tag) |
private void insertContentTag(ElementSpec tag) |
809 |
{ |
{ |
810 |
|
prepareContentInsertion(); |
811 |
int len = tag.getLength(); |
int len = tag.getLength(); |
812 |
int dir = tag.getDirection(); |
int dir = tag.getDirection(); |
813 |
if (dir == ElementSpec.JoinPreviousDirection) |
if (dir == ElementSpec.JoinPreviousDirection) |
814 |
{ |
{ |
815 |
Element prev = getCharacterElement(offset); |
// The mauve tests to this class show that a JoinPrevious insertion |
816 |
BranchElement prevParent = (BranchElement) prev.getParentElement(); |
// does not add any edits to the document event. To me this means |
817 |
Element join = createLeafElement(prevParent, tag.getAttributes(), |
// that nothing is done here. The previous element naturally should |
818 |
prev.getStartOffset(), |
// expand so that it covers the new characters. |
|
Math.max(prev.getEndOffset(), |
|
|
offset + len)); |
|
|
int ind = prevParent.getElementIndex(offset); |
|
|
if (ind == -1) |
|
|
ind = 0; |
|
|
Element[] add = new Element[]{join}; |
|
|
prevParent.replace(ind, 1, add); |
|
|
|
|
|
// Add this action to the document event. |
|
|
ElementEdit edit = new ElementEdit(prevParent, ind, |
|
|
new Element[]{prev}, add); |
|
|
documentEvent.addEdit(edit); |
|
819 |
} |
} |
820 |
else if (dir == ElementSpec.JoinNextDirection) |
else if (dir == ElementSpec.JoinNextDirection) |
821 |
{ |
{ |
822 |
Element next = getCharacterElement(offset + len); |
BranchElement paragraph = (BranchElement) elementStack.peek(); |
823 |
BranchElement nextParent = (BranchElement) next.getParentElement(); |
int currentIndex = paragraph.getElementIndex(offset); |
824 |
Element join = createLeafElement(nextParent, tag.getAttributes(), |
Element current = paragraph.getElement(currentIndex); |
825 |
offset, |
Element next = paragraph.getElement(currentIndex + 1); |
826 |
next.getEndOffset()); |
|
827 |
int ind = nextParent.getElementIndex(offset + len); |
Element newEl1 = createLeafElement(paragraph, |
828 |
if (ind == -1) |
current.getAttributes(), |
829 |
ind = 0; |
current.getStartOffset(), |
830 |
Element[] add = new Element[]{join}; |
offset); |
831 |
nextParent.replace(ind, 1, add); |
Element newEl2 = createLeafElement(paragraph, |
832 |
|
current.getAttributes(), |
833 |
|
offset, |
834 |
|
next.getEndOffset()); |
835 |
|
|
836 |
|
Element[] add = new Element[] {newEl1, newEl2}; |
837 |
|
Element[] remove = new Element[] {current, next}; |
838 |
|
paragraph.replace(currentIndex, 2, add); |
839 |
|
|
840 |
// Add this action to the document event. |
// Add this action to the document event. |
841 |
ElementEdit edit = new ElementEdit(nextParent, ind, |
addEdit(paragraph, currentIndex, remove, add); |
|
new Element[]{next}, add); |
|
|
documentEvent.addEdit(edit); |
|
842 |
} |
} |
843 |
else |
else |
844 |
{ |
{ |
845 |
BranchElement par = (BranchElement) getParagraphElement(offset); |
BranchElement paragraph = (BranchElement) elementStack.peek(); |
846 |
|
int index = paragraph.getElementIndex(offset); |
847 |
int ind = par.getElementIndex(offset); |
Element current = paragraph.getElement(index); |
848 |
|
|
849 |
// Make room for the element. |
Element[] added; |
850 |
// Cut previous element. |
Element[] removed; |
851 |
Element prev = par.getElement(ind); |
Element[] splitRes = split(current, offset, length); |
852 |
if (prev != null && prev.getStartOffset() < offset) |
// Special case for when offset == startOffset or offset == endOffset. |
853 |
|
if (splitRes[0] == null) |
854 |
{ |
{ |
855 |
Element cutPrev = createLeafElement(par, prev.getAttributes(), |
added = new Element[2]; |
856 |
prev.getStartOffset(), |
added[0] = createLeafElement(paragraph, tag.getAttributes(), |
857 |
offset); |
offset, offset + length); |
858 |
Element[] remove = new Element[]{prev}; |
added[1] = splitRes[1]; |
859 |
Element[] add = new Element[]{cutPrev}; |
removed = new Element[0]; |
860 |
if (prev.getEndOffset() > offset + len) |
index++; |
861 |
{ |
} |
862 |
Element rem = createLeafElement(par, prev.getAttributes(), |
else if (current.getStartOffset() == offset) |
863 |
offset + len, |
{ |
864 |
prev.getEndOffset()); |
added = new Element[2]; |
865 |
add = new Element[]{cutPrev, rem}; |
added[0] = createLeafElement(paragraph, tag.getAttributes(), |
866 |
} |
offset, offset + length); |
867 |
|
added[1] = splitRes[1]; |
868 |
par.replace(ind, 1, add); |
removed = new Element[] { current }; |
869 |
documentEvent.addEdit(new ElementEdit(par, ind, remove, add)); |
} |
870 |
ind++; |
else if (current.getEndOffset() - length == offset) |
871 |
|
{ |
872 |
|
added = new Element[2]; |
873 |
|
added[0] = splitRes[0]; |
874 |
|
added[1] = createLeafElement(paragraph, tag.getAttributes(), |
875 |
|
offset, offset + length); |
876 |
|
removed = new Element[] { current }; |
877 |
} |
} |
878 |
// ind now points to the next element. |
else |
879 |
|
{ |
880 |
|
added = new Element[3]; |
881 |
|
added[0] = splitRes[0]; |
882 |
|
added[1] = createLeafElement(paragraph, tag.getAttributes(), |
883 |
|
offset, offset + length); |
884 |
|
added[2] = splitRes[1]; |
885 |
|
removed = new Element[] { current }; |
886 |
|
} |
887 |
|
paragraph.replace(index, removed.length, added); |
888 |
|
addEdit(paragraph, index, removed, added); |
889 |
|
} |
890 |
|
offset += len; |
891 |
|
} |
892 |
|
|
893 |
|
/** |
894 |
|
* Creates a copy of the element <code>clonee</code> that has the parent |
895 |
|
* <code>parent</code>. |
896 |
|
* @param parent the parent of the newly created Element |
897 |
|
* @param clonee the Element to clone |
898 |
|
* @return the cloned Element |
899 |
|
*/ |
900 |
|
public Element clone (Element parent, Element clonee) |
901 |
|
{ |
902 |
|
// If the Element we want to clone is a leaf, then simply copy it |
903 |
|
if (clonee.isLeaf()) |
904 |
|
return createLeafElement(parent, clonee.getAttributes(), |
905 |
|
clonee.getStartOffset(), clonee.getEndOffset()); |
906 |
|
|
907 |
|
// Otherwise create a new BranchElement with the desired parent and |
908 |
|
// the clonee's attributes |
909 |
|
BranchElement result = (BranchElement) createBranchElement(parent, clonee.getAttributes()); |
910 |
|
|
911 |
|
// And clone all the of clonee's children |
912 |
|
Element[] children = new Element[clonee.getElementCount()]; |
913 |
|
for (int i = 0; i < children.length; i++) |
914 |
|
children[i] = clone(result, clonee.getElement(i)); |
915 |
|
|
916 |
|
// Make the cloned children the children of the BranchElement |
917 |
|
result.replace(0, 0, children); |
918 |
|
return result; |
919 |
|
} |
920 |
|
|
921 |
// Cut next element if necessary. |
/** |
922 |
Element next = par.getElement(ind); |
* Adds an ElementChange for a given element modification to the document |
923 |
if (next != null && next.getStartOffset() < offset + len) |
* event. If there already is an ElementChange registered for this element, |
924 |
|
* this method tries to merge the ElementChanges together. However, this |
925 |
|
* is only possible if the indices of the new and old ElementChange are |
926 |
|
* equal. |
927 |
|
* |
928 |
|
* @param e the element |
929 |
|
* @param i the index of the change |
930 |
|
* @param removed the removed elements, or <code>null</code> |
931 |
|
* @param added the added elements, or <code>null</code> |
932 |
|
*/ |
933 |
|
private void addEdit(Element e, int i, Element[] removed, Element[] added) |
934 |
|
{ |
935 |
|
// Perform sanity check first. |
936 |
|
DocumentEvent.ElementChange ec = documentEvent.getChange(e); |
937 |
|
|
938 |
|
// Merge the existing stuff with the new stuff. |
939 |
|
Element[] oldAdded = ec == null ? null: ec.getChildrenAdded(); |
940 |
|
Element[] newAdded; |
941 |
|
if (oldAdded != null && added != null) |
942 |
|
{ |
943 |
|
if (ec.getIndex() <= i) |
944 |
{ |
{ |
945 |
Element cutNext = createLeafElement(par, next.getAttributes(), |
int index = i - ec.getIndex(); |
946 |
offset + len, |
// Merge adds together. |
947 |
next.getEndOffset()); |
newAdded = new Element[oldAdded.length + added.length]; |
948 |
Element[] remove = new Element[]{next}; |
System.arraycopy(oldAdded, 0, newAdded, 0, index); |
949 |
Element[] add = new Element[]{cutNext}; |
System.arraycopy(added, 0, newAdded, index, added.length); |
950 |
par.replace(ind, 1, add); |
System.arraycopy(oldAdded, index, newAdded, index + added.length, |
951 |
documentEvent.addEdit(new ElementEdit(par, ind, remove, |
oldAdded.length - index); |
952 |
add)); |
i = ec.getIndex(); |
953 |
} |
} |
954 |
|
else |
955 |
|
throw new AssertionError("Not yet implemented case."); |
956 |
|
} |
957 |
|
else if (added != null) |
958 |
|
newAdded = added; |
959 |
|
else if (oldAdded != null) |
960 |
|
newAdded = oldAdded; |
961 |
|
else |
962 |
|
newAdded = new Element[0]; |
963 |
|
|
964 |
// Insert new element. |
Element[] oldRemoved = ec == null ? null: ec.getChildrenRemoved(); |
965 |
Element newEl = createLeafElement(par, tag.getAttributes(), |
Element[] newRemoved; |
966 |
offset, offset + len); |
if (oldRemoved != null && removed != null) |
967 |
Element[] added = new Element[]{newEl}; |
{ |
968 |
par.replace(ind, 0, added); |
if (ec.getIndex() <= i) |
969 |
// Add this action to the document event. |
{ |
970 |
ElementEdit edit = new ElementEdit(par, ind, new Element[0], |
int index = i - ec.getIndex(); |
971 |
added); |
// Merge removes together. |
972 |
documentEvent.addEdit(edit); |
newRemoved = new Element[oldRemoved.length + removed.length]; |
973 |
|
System.arraycopy(oldAdded, 0, newRemoved, 0, index); |
974 |
|
System.arraycopy(removed, 0, newRemoved, index, removed.length); |
975 |
|
System.arraycopy(oldRemoved, index, newRemoved, |
976 |
|
index + removed.length, |
977 |
|
oldRemoved.length - index); |
978 |
|
i = ec.getIndex(); |
979 |
|
} |
980 |
|
else |
981 |
|
throw new AssertionError("Not yet implemented case."); |
982 |
} |
} |
983 |
offset += len; |
else if (removed != null) |
984 |
|
newRemoved = removed; |
985 |
|
else if (oldRemoved != null) |
986 |
|
newRemoved = oldRemoved; |
987 |
|
else |
988 |
|
newRemoved = new Element[0]; |
989 |
|
|
990 |
|
// Replace the existing edit for the element with the merged. |
991 |
|
documentEvent.addEdit(new ElementEdit(e, i, newRemoved, newAdded)); |
992 |
} |
} |
993 |
} |
} |
994 |
|
|
1018 |
} |
} |
1019 |
} |
} |
1020 |
|
|
1021 |
|
/** |
1022 |
|
* Receives notification when any of the document's style changes and calls |
1023 |
|
* {@link DefaultStyledDocument#styleChanged(Style)}. |
1024 |
|
* |
1025 |
|
* @author Roman Kennke (kennke@aicas.com) |
1026 |
|
*/ |
1027 |
|
private class StyleChangeListener |
1028 |
|
implements ChangeListener |
1029 |
|
{ |
1030 |
|
|
1031 |
|
/** |
1032 |
|
* Receives notification when any of the document's style changes and calls |
1033 |
|
* {@link DefaultStyledDocument#styleChanged(Style)}. |
1034 |
|
* |
1035 |
|
* @param event the change event |
1036 |
|
*/ |
1037 |
|
public void stateChanged(ChangeEvent event) |
1038 |
|
{ |
1039 |
|
Style style = (Style) event.getSource(); |
1040 |
|
styleChanged(style); |
1041 |
|
} |
1042 |
|
} |
1043 |
|
|
1044 |
/** The serialization UID (compatible with JDK1.5). */ |
/** The serialization UID (compatible with JDK1.5). */ |
1045 |
private static final long serialVersionUID = 940485415728614849L; |
private static final long serialVersionUID = 940485415728614849L; |
1046 |
|
|
1056 |
protected DefaultStyledDocument.ElementBuffer buffer; |
protected DefaultStyledDocument.ElementBuffer buffer; |
1057 |
|
|
1058 |
/** |
/** |
1059 |
|
* Listens for changes on this document's styles and notifies styleChanged(). |
1060 |
|
*/ |
1061 |
|
private StyleChangeListener styleChangeListener; |
1062 |
|
|
1063 |
|
/** |
1064 |
* Creates a new <code>DefaultStyledDocument</code>. |
* Creates a new <code>DefaultStyledDocument</code>. |
1065 |
*/ |
*/ |
1066 |
public DefaultStyledDocument() |
public DefaultStyledDocument() |
1113 |
public Style addStyle(String nm, Style parent) |
public Style addStyle(String nm, Style parent) |
1114 |
{ |
{ |
1115 |
StyleContext context = (StyleContext) getAttributeContext(); |
StyleContext context = (StyleContext) getAttributeContext(); |
1116 |
return context.addStyle(nm, parent); |
Style newStyle = context.addStyle(nm, parent); |
1117 |
|
|
1118 |
|
// Register change listener. |
1119 |
|
if (styleChangeListener == null) |
1120 |
|
styleChangeListener = new StyleChangeListener(); |
1121 |
|
newStyle.addChangeListener(styleChangeListener); |
1122 |
|
|
1123 |
|
return newStyle; |
1124 |
} |
} |
1125 |
|
|
1126 |
/** |
/** |
1164 |
{ |
{ |
1165 |
Element element = getDefaultRootElement(); |
Element element = getDefaultRootElement(); |
1166 |
|
|
1167 |
while (! element.isLeaf()) |
while (!element.isLeaf()) |
1168 |
{ |
{ |
1169 |
int index = element.getElementIndex(position); |
int index = element.getElementIndex(position); |
1170 |
element = element.getElement(index); |
element = element.getElement(index); |
1171 |
} |
} |
1172 |
|
|
1173 |
return element; |
return element; |
1315 |
int paragraphCount = root.getElementCount(); |
int paragraphCount = root.getElementCount(); |
1316 |
for (int pindex = 0; pindex < paragraphCount; pindex++) |
for (int pindex = 0; pindex < paragraphCount; pindex++) |
1317 |
{ |
{ |
1318 |
Element paragraph = root.getElement(pindex); |
Element paragraph = root.getElement(pindex); |
1319 |
// Skip paragraphs that lie outside the interval. |
// Skip paragraphs that lie outside the interval. |
1320 |
if ((paragraph.getStartOffset() > offset + length) |
if ((paragraph.getStartOffset() > offset + length) |
1321 |
|| (paragraph.getEndOffset() < offset)) |
|| (paragraph.getEndOffset() < offset)) |
1322 |
continue; |
continue; |
1323 |
|
|
1324 |
// Visit content elements within this paragraph |
// Visit content elements within this paragraph |
1325 |
int contentCount = paragraph.getElementCount(); |
int contentCount = paragraph.getElementCount(); |
1326 |
for (int cindex = 0; cindex < contentCount; cindex++) |
for (int cindex = 0; cindex < contentCount; cindex++) |
1327 |
{ |
{ |
1328 |
Element content = paragraph.getElement(cindex); |
Element content = paragraph.getElement(cindex); |
1329 |
// Skip content that lies outside the interval. |
// Skip content that lies outside the interval. |
1330 |
if ((content.getStartOffset() > offset + length) |
if ((content.getStartOffset() > offset + length) |
1331 |
|| (content.getEndOffset() < offset)) |
|| (content.getEndOffset() < offset)) |
1332 |
continue; |
continue; |
1333 |
|
|
1334 |
if (content instanceof AbstractElement) |
if (content instanceof AbstractElement) |
1335 |
{ |
{ |
1336 |
AbstractElement el = (AbstractElement) content; |
AbstractElement el = (AbstractElement) content; |
1337 |
if (replace) |
if (replace) |
1338 |
el.removeAttributes(el); |
el.removeAttributes(el); |
1339 |
el.addAttributes(attributes); |
el.addAttributes(attributes); |
1340 |
} |
} |
1341 |
else |
else |
1342 |
throw new AssertionError("content elements are expected to be" |
throw new AssertionError("content elements are expected to be" |
1343 |
+ "instances of " |
+ "instances of " |
1344 |
+ "javax.swing.text.AbstractDocument.AbstractElement"); |
+ "javax.swing.text.AbstractDocument.AbstractElement"); |
1345 |
} |
} |
1346 |
} |
} |
1347 |
|
|
1348 |
fireChangedUpdate(ev); |
fireChangedUpdate(ev); |
1413 |
catch (BadLocationException ex) |
catch (BadLocationException ex) |
1414 |
{ |
{ |
1415 |
AssertionError ae = new AssertionError("Unexpected bad location"); |
AssertionError ae = new AssertionError("Unexpected bad location"); |
1416 |
ae.initCause(ex); |
ae.initCause(ex); |
1417 |
throw ae; |
throw ae; |
1418 |
} |
} |
1419 |
|
|
1420 |
int len = 0; |
int len = 0; |
1483 |
(ElementSpec[]) specs.toArray(new ElementSpec[specs.size()]); |
(ElementSpec[]) specs.toArray(new ElementSpec[specs.size()]); |
1484 |
|
|
1485 |
buffer.insert(offset, length, elSpecs, ev); |
buffer.insert(offset, length, elSpecs, ev); |
1486 |
} |
} |
1487 |
|
|
1488 |
|
/** |
1489 |
|
* Returns an enumeration of all style names. |
1490 |
|
* |
1491 |
|
* @return an enumeration of all style names |
1492 |
|
*/ |
1493 |
|
public Enumeration getStyleNames() |
1494 |
|
{ |
1495 |
|
StyleContext context = (StyleContext) getAttributeContext(); |
1496 |
|
return context.getStyleNames(); |
1497 |
|
} |
1498 |
|
|
1499 |
|
/** |
1500 |
|
* Called when any of this document's styles changes. |
1501 |
|
* |
1502 |
|
* @param style the style that changed |
1503 |
|
*/ |
1504 |
|
protected void styleChanged(Style style) |
1505 |
|
{ |
1506 |
|
// Nothing to do here. This is intended to be overridden by subclasses. |
1507 |
|
} |
1508 |
|
|
1509 |
|
/** |
1510 |
|
* Inserts a bulk of structured content at once. |
1511 |
|
* |
1512 |
|
* @param offset the offset at which the content should be inserted |
1513 |
|
* @param data the actual content spec to be inserted |
1514 |
|
*/ |
1515 |
|
protected void insert(int offset, ElementSpec[] data) |
1516 |
|
throws BadLocationException |
1517 |
|
{ |
1518 |
|
writeLock(); |
1519 |
|
// First we insert the content. |
1520 |
|
int index = offset; |
1521 |
|
for (int i = 0; i < data.length; i++) |
1522 |
|
{ |
1523 |
|
ElementSpec spec = data[i]; |
1524 |
|
if (spec.getArray() != null && spec.getLength() > 0) |
1525 |
|
{ |
1526 |
|
String insertString = new String(spec.getArray(), spec.getOffset(), |
1527 |
|
spec.getLength()); |
1528 |
|
content.insertString(index, insertString); |
1529 |
|
} |
1530 |
|
index += spec.getLength(); |
1531 |
|
} |
1532 |
|
// Update the view structure. |
1533 |
|
DefaultDocumentEvent ev = new DefaultDocumentEvent(offset, index - offset, |
1534 |
|
DocumentEvent.EventType.INSERT); |
1535 |
|
for (int i = 0; i < data.length; i++) |
1536 |
|
{ |
1537 |
|
ElementSpec spec = data[i]; |
1538 |
|
AttributeSet atts = spec.getAttributes(); |
1539 |
|
if (atts != null) |
1540 |
|
insertUpdate(ev, atts); |
1541 |
|
} |
1542 |
|
|
1543 |
|
// Finally we must update the document structure and fire the insert update |
1544 |
|
// event. |
1545 |
|
buffer.insert(offset, index - offset, data, ev); |
1546 |
|
if (ev.modified) |
1547 |
|
fireInsertUpdate(ev); |
1548 |
|
writeUnlock(); |
1549 |
|
} |
1550 |
|
|
1551 |
|
/** |
1552 |
|
* Initializes the <code>DefaultStyledDocument</code> with the specified |
1553 |
|
* data. |
1554 |
|
* |
1555 |
|
* @param data the specification of the content with which the document is |
1556 |
|
* initialized |
1557 |
|
*/ |
1558 |
|
protected void create(ElementSpec[] data) |
1559 |
|
{ |
1560 |
|
try |
1561 |
|
{ |
1562 |
|
// Clear content. |
1563 |
|
content.remove(0, content.length()); |
1564 |
|
// Clear buffer and root element. |
1565 |
|
buffer = new ElementBuffer(createDefaultRoot()); |
1566 |
|
// Insert the data. |
1567 |
|
insert(0, data); |
1568 |
|
} |
1569 |
|
catch (BadLocationException ex) |
1570 |
|
{ |
1571 |
|
AssertionError err = new AssertionError("Unexpected bad location"); |
1572 |
|
err.initCause(ex); |
1573 |
|
throw err; |
1574 |
|
} |
1575 |
|
} |
1576 |
} |
} |