/[classpath]/classpath/javax/swing/text/DefaultStyledDocument.java
ViewVC logotype

Diff of /classpath/javax/swing/text/DefaultStyledDocument.java

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 1.1.2.6 by gnu_andrew, Wed Nov 2 00:44:03 2005 UTC revision 1.1.2.7 by gnu_andrew, Sun Nov 27 21:00:42 2005 UTC
# Line 41  package javax.swing.text; Line 41  package javax.swing.text;
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}.
# Line 61  public class DefaultStyledDocument exten Line 67  public class DefaultStyledDocument exten
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.
# Line 343  public class DefaultStyledDocument exten Line 430  public class DefaultStyledDocument exten
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
# Line 364  public class DefaultStyledDocument exten Line 471  public class DefaultStyledDocument exten
471      public ElementBuffer(Element root)      public ElementBuffer(Element root)
472      {      {
473        this.root = root;        this.root = root;
474          elementStack = new Stack();
475      }      }
476    
477      /**      /**
# Line 407  public class DefaultStyledDocument exten Line 515  public class DefaultStyledDocument exten
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      /**      /**
# Line 419  public class DefaultStyledDocument exten Line 566  public class DefaultStyledDocument exten
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      /**      /**
# Line 477  public class DefaultStyledDocument exten Line 678  public class DefaultStyledDocument exten
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    
# Line 495  public class DefaultStyledDocument exten Line 702  public class DefaultStyledDocument exten
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      /**      /**
# Line 589  public class DefaultStyledDocument exten Line 805  public class DefaultStyledDocument exten
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    
# Line 714  public class DefaultStyledDocument exten Line 1018  public class DefaultStyledDocument exten
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    
# Line 729  public class DefaultStyledDocument exten Line 1056  public class DefaultStyledDocument exten
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()
# Line 781  public class DefaultStyledDocument exten Line 1113  public class DefaultStyledDocument exten
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    /**    /**
# Line 825  public class DefaultStyledDocument exten Line 1164  public class DefaultStyledDocument exten
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;
# Line 976  public class DefaultStyledDocument exten Line 1315  public class DefaultStyledDocument exten
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);
# Line 1074  public class DefaultStyledDocument exten Line 1413  public class DefaultStyledDocument exten
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;
# Line 1144  public class DefaultStyledDocument exten Line 1483  public class DefaultStyledDocument exten
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  }  }

Legend:
Removed from v.1.1.2.6  
changed lines
  Added in v.1.1.2.7

savannah-hackers-public@gnu.org
ViewVC Help
Powered by ViewVC 1.1.26