[Patch][gui] AbstractDocument

[Michael Koch]

Hi list,


I commited the attached patch to add some missing stuff to
javax.swing.text.AbstractDocument.


Michael


2005-01-03  Michael Koch  <konqueror@gmx.de>

	* javax/swing/text/AbstractDocument.java
	(documentFilter): New field.
	(getDocumentFilter): New method.
	(setDocumentFilter): Likewise.
	(dump): Likewise.

-------------- next part --------------
Index: javax/swing/text/AbstractDocument.java
===================================================================
RCS file: /cvs/gcc/gcc/libjava/javax/swing/text/AbstractDocument.java,v
retrieving revision 1.3.8.21
diff -u -r1.3.8.21 AbstractDocument.java
--- javax/swing/text/AbstractDocument.java	2 Jan 2005 12:49:19 -0000	1.3.8.21
+++ javax/swing/text/AbstractDocument.java	3 Jan 2005 16:41:19 -0000
@@ -60,7 +60,9 @@
   implements Document, Serializable
 {
   private static final long serialVersionUID = -116069779446114664L;
+  
   protected static final String BAD_LOCATION = "document location failure";
+  
   public static final String BidiElementName = "bidi level";
   public static final String ContentElementName = "content";
   public static final String ParagraphElementName = "paragraph";
@@ -69,6 +71,8 @@
 
   Content content;
   AttributeContext context;
+  DocumentFilter documentFilter;
+  
   protected EventListenerList listenerList = new EventListenerList();
 
   protected AbstractDocument(Content doc)
@@ -373,6 +377,27 @@
   {
   }
 
+  /**
+   * @since 1.4
+   */
+  public DocumentFilter getDocumentFilter()
+  {
+    return documentFilter;
+  }
+
+  /**
+   * @since 1.4
+   */
+  public void setDocumentFilter(DocumentFilter filter)
+  {
+    this.documentFilter = filter;
+  }
+
+  public void dump(PrintStream out)
+  {
+    ((AbstractElement) getDefaultRootElement()).dump(out, 0);
+  }
+
   public interface AttributeContext
   {
     AttributeSet addAttribute(AttributeSet old, Object name, Object value);
@@ -416,7 +441,6 @@
     AttributeSet attributes;
 
     Element element_parent;
-    Vector element_children;
 
     TreeNode tree_parent;
     Vector tree_children;
@@ -609,7 +633,7 @@
   {
     private static final long serialVersionUID = -8595176318868717313L;
     
-    private Vector children = new Vector();
+    private Element[] children = new Element[0];
 
     public BranchElement(Element parent, AttributeSet attributes)
     {
@@ -618,7 +642,15 @@
 
     public Enumeration children()
     {
-      return children.elements();
+      if (children.length == 0)
+        return null;
+
+      Vector tmp = new Vector();
+
+      for (int index = 0; index < children.length; ++index)
+	tmp.add(children[index]);
+      
+      return tmp.elements();
     }
 
     public boolean getAllowsChildren()
@@ -628,33 +660,36 @@
 
     public Element getElement(int index)
     {
-      if (index < 0 || index >= children.size())
+      if (index < 0 || index >= children.length)
 	return null;
 
-      return (Element) children.get(index);
+      return children[index];
     }
 
     public int getElementCount()
     {
-      return children.size();
+      return children.length;
     }
 
     public int getElementIndex(int offset)
     {
-      if (children.size() == 0)
-	return 0;
-      
-      Element element = positionToElement(offset);
+      // XXX: There is surely a better algorithm
+      // as beginning from first element each time.
+      for (int index = 0; index < children.length; ++index)
+        {
+	  Element elem = children[index];
 
-      if (element == null)
-	return 0;
-      
-      return children.indexOf(element);
+	  if ((elem.getStartOffset() <= offset)
+	      && (offset < elem.getEndOffset()))
+	    return index;
+        }
+
+      return 0;
     }
 
     public int getEndOffset()
     {
-      return ((Element) children.lastElement()).getEndOffset();
+      return children[children.length - 1].getEndOffset();
     }
 
     public String getName()
@@ -664,7 +699,7 @@
 
     public int getStartOffset()
     {
-      return ((Element) children.firstElement()).getStartOffset();
+      return children[0].getStartOffset();
     }
 
     public boolean isLeaf()
@@ -676,9 +711,9 @@
     {
       // XXX: There is surely a better algorithm
       // as beginning from first element each time.
-      for (int index = 0; index < children.size(); ++index)
+      for (int index = 0; index < children.length; ++index)
         {
-	  Element elem = (Element) children.get(index);
+	  Element elem = children[index];
 
 	  if ((elem.getStartOffset() <= position)
 	      && (position < elem.getEndOffset()))
@@ -688,13 +723,16 @@
       return null;
     }
 
-    public void replace(int offset, int length, Element[] elems)
+    public void replace(int offset, int length, Element[] elements)
     {
-      for (int index = 0; index < length; ++index)
-	children.removeElementAt(offset);
-
-      for (int index = 0; index < elems.length; ++index)
-	children.add(offset + index, elems[index]);
+      Element[] target = new Element[children.length - length
+				     + elements.length];
+      System.arraycopy(children, 0, target, 0, offset);
+      System.arraycopy(elements, 0, target, offset, elements.length);
+      System.arraycopy(children, offset + length, target,
+		       offset + elements.length,
+		       children.length - offset - length);
+      children = target;
     }
 
     public String toString()