defaultstyleddocument.java

gcc的组建

    }

    /**
     * Modifies the element structure so that the specified interval starts
     * and ends at an element boundary. Content and paragraph elements
     * are split and created as necessary.
     *
     * This also updates the <code>DefaultDocumentEvent</code> to reflect the
     * structural changes.
     *
     * The bulk work is delegated to {@link #changeUpdate()}.
     *
     * @param offset the start index of the interval to be changed
     * @param length the length of the interval to be changed
     * @param ev the <code>DefaultDocumentEvent</code> describing the change
     */
    public void change(int offset, int length, DefaultDocumentEvent ev)
    {
      this.offset = offset;
      this.length = length;
      documentEvent = ev;
      changeUpdate();
    }

    /**
     * Performs the actual work for {@link #change}.
     * The elements at the interval boundaries are split up (if necessary)
     * so that the interval boundaries are located at element boundaries.
     */
    protected void changeUpdate()
    {
      // Split up the element at the start offset if necessary.
      Element el = getCharacterElement(offset);
      split(el, offset);

      int endOffset = offset + length;
      el = getCharacterElement(endOffset);
      split(el, endOffset);
    }

    /**
     * Splits an element if <code>offset</code> is not alread at its boundary.
     *
     * @param el the Element to possibly split
     * @param offset the offset at which to possibly split
     */
    void split(Element el, int offset)
    {
      if (el instanceof AbstractElement)
        {
          AbstractElement ael = (AbstractElement) el;
          int startOffset = ael.getStartOffset();
          int endOffset = ael.getEndOffset();
          int len = endOffset - startOffset;
          if (startOffset != offset && endOffset != offset)
            {
              Element paragraph = ael.getParentElement();
              if (paragraph instanceof BranchElement)
                {
                  BranchElement par = (BranchElement) paragraph;
                  Element child1 = createLeafElement(par, ael, startOffset,
                                                     offset);
                  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));
                }
              else
                throw new AssertionError("paragraph elements are expected to "
                                         + "be instances of "
			  + "javax.swing.text.AbstractDocument.BranchElement");
            }
        }
      else
        throw new AssertionError("content elements are expected to be "
                                 + "instances of "
			+ "javax.swing.text.AbstractDocument.AbstractElement");
    }

    /**
     * Inserts new <code>Element</code> in the document at the specified
     * position.
     *
     * Most of the work is done by {@link #insertUpdate}, after some fields
     * have been prepared for it.
     *
     * @param offset the location in the document at which the content is
     *        inserted
     * @param length the length of the inserted content
     * @param data the element specifications for the content to be inserted
     * @param ev the document event that is updated to reflect the structural
     *        changes
     */
    public void insert(int offset, int length, ElementSpec[] data,
                       DefaultDocumentEvent ev)
    {
      this.offset = offset;
      this.length = length;
      documentEvent = ev;
      insertUpdate(data);
    }

    /**
     * Performs the actual structural change for {@link #insert}. This
     * creates a bunch of {@link Element}s as specified by <code>data</code>
     * and inserts it into the document as specified in the arguments to
     * {@link #insert}.
     *
     * @param data the element specifications for the elements to be inserte
     */
    protected void insertUpdate(ElementSpec[] data)
    {
      for (int i = 0; i < data.length; i++)
        {
          switch (data[i].getType())
            {
            case ElementSpec.StartTagType:
              insertStartTag(data[i]);
              break;
            case ElementSpec.EndTagType:
              insertEndTag(data[i]);
              break;
            default:
              insertContentTag(data[i]);
              break;
            }
        }
    }

    /**
     * Insert a new paragraph after the paragraph at the current position.
     *
     * @param tag the element spec that describes the element to be inserted
     */
    void insertStartTag(ElementSpec tag)
    {
      BranchElement root = (BranchElement) getDefaultRootElement();
      int index = root.getElementIndex(offset);
      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);

      // Maybe add fractured elements.
      if (tag.getDirection() == ElementSpec.JoinFractureDirection)
        {
          Element[] newFracture = new Element[fracture.length];
          for (int i = 0; i < fracture.length; i++)
            {
              Element oldLeaf = fracture[i];
              Element newLeaf = createLeafElement(newParagraph,
                                                  oldLeaf.getAttributes(),
                                                  oldLeaf.getStartOffset(),
                                                  oldLeaf.getEndOffset());
              newFracture[i] = newLeaf;
            }
          newParagraph.replace(0, 0, newFracture);
          edit = new ElementEdit(newParagraph, 0, new Element[0],
                                 fracture);
          documentEvent.addEdit(edit);
          fracture = new Element[0];
        }
    }

    /**
     * Inserts an end tag into the document structure. This cuts of the
     * current paragraph element, possibly fracturing it's child elements.
     * The fractured elements are saved so that they can be joined later
     * with a new paragraph element.
     */
    void insertEndTag(ElementSpec tag)
    {
      BranchElement root = (BranchElement) getDefaultRootElement();
      int parIndex = root.getElementIndex(offset);
      BranchElement paragraph = (BranchElement) root.getElement(parIndex);

      int index = paragraph.getElementIndex(offset);
      LeafElement content = (LeafElement) paragraph.getElement(index);
      // We might have to split the element at offset.
      split(content, offset);
      index = paragraph.getElementIndex(offset);

      int count = paragraph.getElementCount();
      // Store fractured elements.
      fracture = new Element[count - index];
      for (int i = index; i < count; ++i)
        fracture[i - index] = paragraph.getElement(i);

      // Delete fractured elements.
      paragraph.replace(index, count - index, new Element[0]);

      // Add this action to the document event.
      ElementEdit edit = new ElementEdit(paragraph, index, fracture,
                                         new Element[0]);
      documentEvent.addEdit(edit);
    }

    /**
     * Inserts a content element into the document structure.
     *
     * @param tag the element spec
     */
    void insertContentTag(ElementSpec tag)
    {
      int len = tag.getLength();
      int dir = tag.getDirection();
      if (dir == ElementSpec.JoinPreviousDirection)
        {
          Element prev = getCharacterElement(offset);
          BranchElement prevParent = (BranchElement) prev.getParentElement();
          Element join = createLeafElement(prevParent, tag.getAttributes(),
                                           prev.getStartOffset(),
                                           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);
        }
      else if (dir == ElementSpec.JoinNextDirection)
        {
          Element next = getCharacterElement(offset + len);
          BranchElement nextParent = (BranchElement) next.getParentElement();
          Element join = createLeafElement(nextParent, tag.getAttributes(),
                                           offset,
                                           next.getEndOffset());
          int ind = nextParent.getElementIndex(offset + len);
          if (ind == -1)
            ind = 0;
          Element[] add = new Element[]{join};
          nextParent.replace(ind, 1, add);

          // Add this action to the document event.
          ElementEdit edit = new ElementEdit(nextParent, ind,
                                             new Element[]{next}, add);
          documentEvent.addEdit(edit);
        }
      else
        {
          BranchElement par = (BranchElement) getParagraphElement(offset);

          int ind = par.getElementIndex(offset);

          // Make room for the element.
          // Cut previous element.
          Element prev = par.getElement(ind);
          if (prev != null && prev.getStartOffset() < offset)
            {
              Element cutPrev = createLeafElement(par, prev.getAttributes(),
                                                  prev.getStartOffset(),
                                                  offset);
              Element[] remove = new Element[]{prev};
              Element[] add = new Element[]{cutPrev};
              if (prev.getEndOffset() > offset + len)
                {
                  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++;
            }
          // ind now points to the next element.

          // Cut next element if necessary.
          Element next = par.getElement(ind);
          if (next != null && next.getStartOffset() < offset + len)
            {
              Element cutNext = createLeafElement(par, next.getAttributes(),
                                                  offset + len,
                                                  next.getEndOffset());
              Element[] remove = new Element[]{next};
              Element[] add = new Element[]{cutNext};
              par.replace(ind, 1, add);
              documentEvent.addEdit(new ElementEdit(par, ind, remove,
                                                    add));
            }

          // Insert new element.
          Element newEl = createLeafElement(par, tag.getAttributes(),
                                            offset, offset + len);
          Element[] added = new Element[]{newEl};
          par.replace(ind, 0, added);
          // Add this action to the document event.
          ElementEdit edit = new ElementEdit(par, ind, new Element[0],
                                             added);
          documentEvent.addEdit(edit);
        }
      offset += len;
    }
    
    /**
     * Creates a copy of the element <code>clonee</code> that has the parent
     * <code>parent</code>.
     * @param parent the parent of the newly created Element
     * @param clonee the Element to clone
     * @return the cloned Element
     */
    public Element clone (Element parent, Element clonee)
    {
      // If the Element we want to clone is a leaf, then simply copy it
      if (clonee.isLeaf())
        return createLeafElement(parent, clonee.getAttributes(),
                                 clonee.getStartOffset(), clonee.getEndOffset());
      
      // Otherwise create a new BranchElement with the desired parent and 
      // the clonee's attributes
      BranchElement result = (BranchElement) createBranchElement(parent, clonee.getAttributes());
      
      // And clone all the of clonee's children
      Element[] children = new Element[clonee.getElementCount()];
      for (int i = 0; i < children.length; i++)
        children[i] = clone(result, clonee.getElement(i));
      
      // Make the cloned children the children of the BranchElement
      result.replace(0, 0, children);
      return result;
    }
  }

  /**
   * An element type for sections. This is a simple BranchElement with
   * a unique name.
   */
  protected class SectionElement extends BranchElement
  {
    /**
     * Creates a new SectionElement.
     */
    public SectionElement()
    {
      super(null, null);
    }

    /**
     * Returns the name of the element. This method always returns
     * &quot;section&quot;.
     *
     * @return the name of the element
     */
    public String getName()
    {
      return "section";
    }
  }

  /**
   * Receives notification when any of the document's style changes and calls
   * {@link DefaultStyledDocument#styleChanged(Style)}.
   *
   * @author Roman Kennke ([e-mail])
   */
  private class StyleChangeListener
    implements ChangeListener
  {

    /**
     * Receives notification when any of the document's style changes and calls
     * {@link DefaultStyledDocument#styleChanged(Style)}.
     *
     * @param event the change event
     */
    public void stateChanged(ChangeEvent event)
    {
      Style style = (Style) event.getSource();
      styleChanged(style);
    }
  }

  /** The serialization UID (compatible with JDK1.5). */
  private static final long serialVersionUID = 940485415728614849L;

  /**
   * The default size to use for new content buffers.
   */
  public static final int BUFFER_SIZE_DEFAULT = 4096;

  /**
   * The <code>EditorBuffer</code> that is used to manage to
   * <code>Element</code> hierarchy.
   */
  protected DefaultStyledDocument.ElementBuffer buffer;

  /**
   * Listens for changes on this document's styles and notifies styleChanged().
   */
  private StyleChangeListener styleChangeListener;

  /**
   * Creates a new <code>DefaultStyledDocument</code>.
   */
  public DefaultStyledDocument()
  {
    this(new GapContent(BUFFER_SIZE_DEFAULT), new StyleContext());
  }

  /**
   * Creates a new <code>DefaultStyledDocument</code> that uses the
   * specified {@link StyleContext}.
   *
   * @param context the <code>StyleContext</code> to use
   */
  public DefaultStyledDocument(StyleContext context)
  {
    this(new GapContent(BUFFER_SIZE_DEFAULT), context);
  }

  /**
   * Creates a new <code>DefaultStyledDocument</code> that uses the
   * specified {@link StyleContext} and {@link Content} buffer.
   *
   * @param content the <code>Content</code> buffer to use
   * @param context the <code>StyleContext</code> to use
   */
  public DefaultStyledDocument(AbstractDocument.Content content,
			       StyleContext context)
  {
    super(content, context);
    buffer = new ElementBuffer(createDefaultRoot());
    setLogicalStyle(0, context.getStyle(StyleContext.DEFAULT_STYLE));
  }

  /**
   * Adds a style into the style hierarchy. Unspecified style attributes
   * can be resolved in the <code>parent</code> style, if one is specified.
   *
   * While it is legal to add nameless styles (<code>nm == null</code),
   * you must be aware that the client application is then responsible
   * for managing the style hierarchy, since unnamed styles cannot be
   * looked up by their name.
   *
   * @param nm the name of the style or <code>null</code> if the style should
   *           be unnamed
   * @param parent the parent in which unspecified style attributes are
   *           resolved, or <code>null</code> if that is not necessary
   *
   * @return the newly created <code>Style</code>
   */
  public Style addStyle(String nm, Style parent)
  {