/[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.17 by abalkiss, Tue Nov 8 16:43:29 2005 UTC revision 1.18 by rabbit78, Wed Nov 23 14:12:39 2005 UTC
# Line 42  import java.awt.Color; Line 42  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;  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;  import javax.swing.event.ChangeEvent;
# Line 429  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 450  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 493  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 505  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         *         be splitted can remain in place. The second element might also
575         *         be null, which means that the offset is already at an element
576         *         boundary and the element doesn't need to be splitted.
577         *          
578         */
579        private Element[] split(Element el, int offset, int space)
580        {
581          // If we are at an element boundary, then return an empty array.
582          if ((offset == el.getStartOffset() || offset == el.getEndOffset())
583              && space == 0 && el.isLeaf())
584            return new Element[2];
585    
586          // If the element is an instance of BranchElement, then we recursivly
587          // call this method to perform the split.
588          Element[] res = new Element[2];
589          if (el instanceof BranchElement)
590          {          {
591            AbstractElement ael = (AbstractElement) el;            int index = el.getElementIndex(offset);
592            int startOffset = ael.getStartOffset();            Element child = el.getElement(index);
593            int endOffset = ael.getEndOffset();            Element[] result = split(child, offset, space);
594            int len = endOffset - startOffset;            Element[] removed;
595            if (startOffset != offset && endOffset != offset)            Element[] added;
596              Element[] newAdded;
597    
598              int count = el.getElementCount();
599              if (!(result[1] == null))
600              {              {
601                Element paragraph = ael.getParentElement();                // This is the case when we can keep the first element.
602                if (paragraph instanceof BranchElement)                if (result[0] == null)
603                  {                  {
604                    BranchElement par = (BranchElement) paragraph;                    removed = new Element[count - index - 1];
605                    Element child1 = createLeafElement(par, ael, startOffset,                    newAdded = new Element[count - index - 1];
606                                                       offset);                    added = new Element[]{};
                   Element child2 = createLeafElement(par, ael, offset,  
                                                      endOffset);  
                   int index = par.getElementIndex(startOffset);  
                   Element[] add = new Element[]{ child1, child2 };  
                   par.replace(index, 1, add);  
                   documentEvent.addEdit(new ElementEdit(par, index,  
                                                         new Element[]{ el },  
                                                         add));  
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                  newAdded[0] = result[1];
616                  for (int i = index; i < count; i++)
617                    {
618                      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        else if (el instanceof LeafElement)
650          throw new AssertionError("content elements are expected to be "          {
651                                   + "instances of "            BranchElement par = (BranchElement) el.getParentElement();
652                          + "javax.swing.text.AbstractDocument.AbstractElement");            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 563  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 581  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 675  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++;
                 {  
                   Element rem = createLeafElement(par, prev.getAttributes(),  
                                                   offset + len,  
                                                   prev.getEndOffset());  
                   add = new Element[]{cutPrev, rem};  
                 }  
   
               par.replace(ind, 1, add);  
               documentEvent.addEdit(new ElementEdit(par, ind, remove, add));  
               ind++;  
861              }              }
862            // ind now points to the next element.            else if (current.getStartOffset() == offset)
   
           // Cut next element if necessary.  
           Element next = par.getElement(ind);  
           if (next != null && next.getStartOffset() < offset + len)  
863              {              {
864                Element cutNext = createLeafElement(par, next.getAttributes(),                added = new Element[2];
865                                                    offset + len,                added[0] = createLeafElement(paragraph, tag.getAttributes(),
866                                                    next.getEndOffset());                                             offset, offset + length);
867                Element[] remove = new Element[]{next};                added[1] = splitRes[1];
868                Element[] add = new Element[]{cutNext};                removed = new Element[] { current };
               par.replace(ind, 1, add);  
               documentEvent.addEdit(new ElementEdit(par, ind, remove,  
                                                     add));  
869              }              }
870              else if (current.getEndOffset() - length == offset)
871            // Insert new element.              {
872            Element newEl = createLeafElement(par, tag.getAttributes(),                added = new Element[2];
873                                              offset, offset + len);                added[0] = splitRes[0];
874            Element[] added = new Element[]{newEl};                added[1] = createLeafElement(paragraph, tag.getAttributes(),
875            par.replace(ind, 0, added);                                             offset, offset + length);
876            // Add this action to the document event.                removed = new Element[] { current };
877            ElementEdit edit = new ElementEdit(par, ind, new Element[0],              }
878                                               added);            else
879            documentEvent.addEdit(edit);              {
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;        offset += len;
891      }      }
# Line 800  public class DefaultStyledDocument exten Line 917  public class DefaultStyledDocument exten
917        result.replace(0, 0, children);        result.replace(0, 0, children);
918        return result;        return result;
919      }      }
920    
921        /**
922         * Adds an ElementChange for a given element modification to the document
923         * 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                  int index = i - ec.getIndex();
946                  // Merge adds together.
947                  newAdded = new Element[oldAdded.length + added.length];
948                  System.arraycopy(oldAdded, 0, newAdded, 0, index);
949                  System.arraycopy(added, 0, newAdded, index, added.length);
950                  System.arraycopy(oldAdded, index, newAdded, index + added.length,
951                                   oldAdded.length - index);
952                  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          Element[] oldRemoved = ec == null ? null: ec.getChildrenRemoved();
965          Element[] newRemoved;
966          if (oldRemoved != null && removed != null)
967            {
968              if (ec.getIndex() <= i)
969                {
970                  int index = i - ec.getIndex();
971                  // Merge removes together.
972                  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          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    
995    /**    /**
# Line 1353  public class DefaultStyledDocument exten Line 1543  public class DefaultStyledDocument exten
1543      // Finally we must update the document structure and fire the insert update      // Finally we must update the document structure and fire the insert update
1544      // event.      // event.
1545      buffer.insert(offset, index - offset, data, ev);      buffer.insert(offset, index - offset, data, ev);
1546      fireInsertUpdate(ev);      if (ev.modified)
1547          fireInsertUpdate(ev);
1548      writeUnlock();      writeUnlock();
1549    }    }
1550    

Legend:
Removed from v.1.17  
changed lines
  Added in v.1.18

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