X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=Robust%2Fsrc%2FClassLibrary%2FVector.java;h=adcd4efa6f296556f6a77ff1c015c09ffa0c1779;hb=57888a70a5a1d240517f542b7b3245086a94e0c8;hp=f4d1f954d1172b50c8458a711719eca2d2ff837e;hpb=0ee61d04531ba8669f3ce4e7d597766f7c4904d3;p=IRC.git

diff --git a/Robust/src/ClassLibrary/Vector.java b/Robust/src/ClassLibrary/Vector.java
index f4d1f954..adcd4efa 100644
--- a/Robust/src/ClassLibrary/Vector.java
+++ b/Robust/src/ClassLibrary/Vector.java
@@ -9,12 +9,24 @@ public class Vector {
     array=new Object[10];
   }
 
-  public Vector( int size ) {
+  public Vector(int size) {
     capacityIncrement=0;
     this.size=0;
     array=new Object[size];
   }
 
+  //used for internal cloning
+  private Vector(int size, int capacityIncrement, Object[] array) {
+    this.size = size;
+    this.capacityIncrement = capacityIncrement;
+    this.array = new Object[array.length];
+    System.arraycopy(array, 0, this.array, 0, size);
+  }
+
+  public Vector clone() {
+    return new Vector(size,capacityIncrement, array);
+  }
+
   public boolean isEmpty() {
     return size==0;
   }
@@ -31,7 +43,7 @@ public class Vector {
   public int indexOf(Object elem, int index) {
     for(int i=index; i<size; i++) {
       if (elem.equals(array[i]))
-	return i;
+        return i;
     }
     return -1;
   }
@@ -40,10 +52,14 @@ public class Vector {
     return indexOf(e)!=-1;
   }
 
-  public void remove(Object o) {
+  public boolean  remove(Object o) {
     int in=indexOf(o);
-    if (in!=-1)
+    if (in!=-1) {
       removeElementAt(in);
+      return true;
+    }
+
+    return false;
   }
 
   public Object elementAt(int index) {
@@ -64,18 +80,18 @@ public class Vector {
     }
   }
 
-  private ensureCapacity(int minCapacity) {
+  private void ensureCapacity(int minCapacity) {
     if (minCapacity>array.length) {
       int newsize;
       if (capacityIncrement<=0)
-	newsize=array.length*2;
+        newsize=array.length*2;
       else
-	newsize=array.length+capacityIncrement;
+        newsize=array.length+capacityIncrement;
       if (newsize<minCapacity)
-	newsize=minCapacity;
+        newsize=minCapacity;
       Object [] newarray=new Object[newsize];
       for(int i=0; i<size; i++)
-	newarray[i]=array[i];
+        newarray[i]=array[i];
       array=newarray;
     }
   }