Source for javax.swing.text.GapContent

   1: /* GapContent.java --
   2:    Copyright (C) 2002, 2004, 2005, 2006 Free Software Foundation, Inc.
   3: 
   4: This file is part of GNU Classpath.
   5: 
   6: GNU Classpath is free software; you can redistribute it and/or modify
   7: it under the terms of the GNU General Public License as published by
   8: the Free Software Foundation; either version 2, or (at your option)
   9: any later version.
  10: 
  11: GNU Classpath is distributed in the hope that it will be useful, but
  12: WITHOUT ANY WARRANTY; without even the implied warranty of
  13: MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
  14: General Public License for more details.
  15: 
  16: You should have received a copy of the GNU General Public License
  17: along with GNU Classpath; see the file COPYING.  If not, write to the
  18: Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
  19: 02110-1301 USA.
  20: 
  21: Linking this library statically or dynamically with other modules is
  22: making a combined work based on this library.  Thus, the terms and
  23: conditions of the GNU General Public License cover the whole
  24: combination.
  25: 
  26: As a special exception, the copyright holders of this library give you
  27: permission to link this library with independent modules to produce an
  28: executable, regardless of the license terms of these independent
  29: modules, and to copy and distribute the resulting executable under
  30: terms of your choice, provided that you also meet, for each linked
  31: independent module, the terms and conditions of the license of that
  32: module.  An independent module is a module which is not derived from
  33: or based on this library.  If you modify this library, you may extend
  34: this exception to your version of the library, but you are not
  35: obligated to do so.  If you do not wish to do so, delete this
  36: exception statement from your version. */
  37: 
  38: 
  39: package javax.swing.text;
  40: 
  41: import java.io.Serializable;
  42: import java.util.Iterator;
  43: import java.util.Set;
  44: import java.util.Vector;
  45: import java.util.WeakHashMap;
  46: 
  47: import javax.swing.undo.AbstractUndoableEdit;
  48: import javax.swing.undo.CannotRedoException;
  49: import javax.swing.undo.CannotUndoException;
  50: import javax.swing.undo.UndoableEdit;
  51: 
  52: /**
  53:  * This implementation of {@link AbstractDocument.Content} uses a gapped buffer.
  54:  * This takes advantage of the fact that text area content is mostly inserted
  55:  * sequentially. The buffer is a char array that maintains a gap at the current
  56:  * insertion point. If characters a inserted at gap boundaries, the cost is
  57:  * minimal (simple array access). The array only has to be shifted around when
  58:  * the insertion point moves (then the gap also moves and one array copy is
  59:  * necessary) or when the gap is filled up and the buffer has to be enlarged.
  60:  */
  61: public class GapContent
  62:     implements AbstractDocument.Content, Serializable
  63: {
  64:   
  65:   /**
  66:    * A {@link Position} implementation for <code>GapContent</code>.
  67:    */
  68:   private class GapContentPosition
  69:     implements Position
  70:   {
  71: 
  72:     /**
  73:      * The index to the positionMarks array entry, which in turn holds the
  74:      * mark into the buffer array.
  75:      */
  76:     int index;
  77: 
  78:     /**
  79:      * Creates a new GapContentPosition object.
  80:      * 
  81:      * @param mark the mark of this Position
  82:      */
  83:     GapContentPosition(int mark)
  84:     {
  85:       // Try to find the mark in the positionMarks array, and store the index
  86:       // to it.
  87:       synchronized (GapContent.this)
  88:         {
  89:           int i = binarySearch(positionMarks, mark, numMarks);
  90:           if (i >= 0) // mark found
  91:             {
  92:               index = i;
  93:             }
  94:           else
  95:             {
  96:               index = -i - 1;
  97:               insertMark(index, mark);
  98:             }
  99:         }
 100:     }
 101: 
 102:     /**
 103:      * Returns the current offset of this Position within the content.
 104:      * 
 105:      * @return the current offset of this Position within the content.
 106:      */
 107:     public int getOffset()
 108:     {
 109:       synchronized (GapContent.this)
 110:         {
 111:           // Fetch the actual mark.
 112:           int mark = positionMarks[index];
 113:           // Check precondition.
 114:           assert mark <= gapStart || mark >= gapEnd : "mark: " + mark
 115:                                                    + ", gapStart: " + gapStart
 116:                                                    + ", gapEnd: " + gapEnd;
 117:           int res = mark;
 118:           if (mark > gapStart)
 119:             res -= (gapEnd - gapStart);
 120:           return res;
 121:         }
 122:     }
 123:   }
 124: 
 125:   private class InsertUndo extends AbstractUndoableEdit
 126:   {
 127:     public int where, length;
 128:     String text;
 129:     public InsertUndo(int start, int len)
 130:     {
 131:       where = start;
 132:       length = len;
 133:     }
 134: 
 135:     public void undo () throws CannotUndoException
 136:     {
 137:       super.undo();
 138:       try
 139:       {
 140:         text = getString(where, length);
 141:         remove(where, length);
 142:       }
 143:       catch (BadLocationException ble)
 144:       {
 145:         throw new CannotUndoException();
 146:       }
 147:     }
 148:     
 149:     public void redo () throws CannotUndoException
 150:     {
 151:       super.redo();
 152:       try
 153:       {
 154:         insertString(where, text);
 155:       }
 156:       catch (BadLocationException ble)
 157:       {
 158:         throw new CannotRedoException();
 159:       }
 160:     }
 161:     
 162:   }
 163:   
 164:   private class UndoRemove extends AbstractUndoableEdit
 165:   {
 166:     public int where;
 167:     String text;
 168:     public UndoRemove(int start, String removedText)
 169:     {
 170:       where = start;
 171:       text = removedText;
 172:     }
 173: 
 174:     public void undo () throws CannotUndoException
 175:     {
 176:       super.undo();
 177:       try
 178:       {
 179:         insertString(where, text);
 180:       }
 181:       catch (BadLocationException ble)
 182:       {
 183:         throw new CannotUndoException();
 184:       }
 185:     }
 186:     
 187:     public void redo () throws CannotUndoException
 188:     {
 189:       super.redo();
 190:       try
 191:       {
 192:         remove(where, text.length());
 193:       }
 194:       catch (BadLocationException ble)
 195:       {
 196:         throw new CannotRedoException();
 197:       }
 198:     }
 199:     
 200:   }
 201: 
 202:   /** The serialization UID (compatible with JDK1.5). */
 203:   private static final long serialVersionUID = -6226052713477823730L;
 204: 
 205:   /**
 206:    * This is the default buffer size and the amount of bytes that a buffer is
 207:    * extended if it is full.
 208:    */
 209:   static final int DEFAULT_BUFSIZE = 10;
 210: 
 211:   /**
 212:    * The text buffer.
 213:    */
 214:   char[] buffer;
 215: 
 216:   /**
 217:    * The index of the first character of the gap.
 218:    */
 219:   int gapStart;
 220: 
 221:   /**
 222:    * The index of the character after the last character of the gap.
 223:    */
 224:   int gapEnd;
 225: 
 226:   // FIXME: We might want to track GC'ed GapContentPositions and remove their
 227:   // corresponding marks, or alternativly, perform some regular cleanup of
 228:   // the positionMarks array.
 229: 
 230:   /**
 231:    * Holds the marks for positions. These marks are referenced by the
 232:    * GapContentPosition instances by an index into this array.
 233:    */
 234:   int[] positionMarks;
 235: 
 236:   /**
 237:    * The number of elements in the positionMarks array. The positionMarks array
 238:    * might be bigger than the actual number of elements.
 239:    */
 240:   int numMarks;
 241: 
 242:   /**
 243:    * (Weakly) Stores the GapContentPosition instances. 
 244:    */
 245:   WeakHashMap positions;
 246: 
 247:   /**
 248:    * Creates a new GapContent object.
 249:    */
 250:   public GapContent()
 251:   {
 252:     this(DEFAULT_BUFSIZE);
 253:   }
 254: 
 255:   /**
 256:    * Creates a new GapContent object with a specified initial size.
 257:    * 
 258:    * @param size the initial size of the buffer
 259:    */
 260:   public GapContent(int size)
 261:   {
 262:     size = Math.max(size, 2);
 263:     buffer = (char[]) allocateArray(size);
 264:     gapStart = 1;
 265:     gapEnd = size;
 266:     buffer[0] = '\n';
 267:     positions = new WeakHashMap();
 268:     positionMarks = new int[10];
 269:     numMarks = 0;
 270:   }
 271: 
 272:   /**
 273:    * Allocates an array of the specified length that can then be used as
 274:    * buffer.
 275:    * 
 276:    * @param size the size of the array to be allocated
 277:    * 
 278:    * @return the allocated array
 279:    */
 280:   protected Object allocateArray(int size)
 281:   {
 282:     return new char[size];
 283:   }
 284: 
 285:   /**
 286:    * Returns the length of the allocated buffer array.
 287:    * 
 288:    * @return the length of the allocated buffer array
 289:    */
 290:   protected int getArrayLength()
 291:   {
 292:     return buffer.length;
 293:   }
 294: 
 295:   /**
 296:    * Returns the length of the content.
 297:    * 
 298:    * @return the length of the content
 299:    */
 300:   public int length()
 301:   {
 302:     return buffer.length - (gapEnd - gapStart);
 303:   }
 304: 
 305:   /**
 306:    * Inserts a string at the specified position.
 307:    * 
 308:    * @param where the position where the string is inserted
 309:    * @param str the string that is to be inserted
 310:    * 
 311:    * @return an UndoableEdit object
 312:    * 
 313:    * @throws BadLocationException if <code>where</code> is not a valid
 314:    *         location in the buffer
 315:    */
 316:   public UndoableEdit insertString(int where, String str)
 317:       throws BadLocationException
 318:   {
 319:     // check arguments
 320:     int length = length();
 321:     int strLen = str.length();
 322: 
 323:     if (where < 0)
 324:       throw new BadLocationException("The where argument cannot be smaller"
 325:                                      + " than the zero", where);
 326: 
 327:     if (where > length)
 328:       throw new BadLocationException("The where argument cannot be greater"
 329:           + " than the content length", where);
 330: 
 331:     replace(where, 0, str.toCharArray(), strLen);
 332: 
 333:     return new InsertUndo(where, strLen);
 334:   }
 335: 
 336:   /**
 337:    * Removes a piece of content at th specified position.
 338:    * 
 339:    * @param where the position where the content is to be removed
 340:    * @param nitems number of characters to be removed
 341:    * 
 342:    * @return an UndoableEdit object
 343:    * 
 344:    * @throws BadLocationException if <code>where</code> is not a valid
 345:    *         location in the buffer
 346:    */
 347:   public UndoableEdit remove(int where, int nitems) throws BadLocationException
 348:   {
 349:     // check arguments
 350:     int length = length();
 351:     
 352:     if ((where + nitems) >= length)
 353:       throw new BadLocationException("where + nitems cannot be greater"
 354:           + " than the content length", where + nitems);
 355:     
 356:     String removedText = getString(where, nitems);
 357:     replace(where, nitems, null, 0);
 358: 
 359:     return new UndoRemove(where, removedText);
 360:   }
 361: 
 362:   /**
 363:    * Returns a piece of content as String.
 364:    * 
 365:    * @param where the start location of the fragment
 366:    * @param len the length of the fragment
 367:    * 
 368:    * @throws BadLocationException if <code>where</code> or
 369:    *         <code>where + len</code> are no valid locations in the buffer
 370:    */
 371:   public String getString(int where, int len) throws BadLocationException
 372:   {
 373:     Segment seg = new Segment();
 374:     try
 375:       {
 376:         getChars(where, len, seg);
 377:         return new String(seg.array, seg.offset, seg.count);
 378:       }
 379:     catch (StringIndexOutOfBoundsException ex)
 380:       {
 381:         int invalid = 0;
 382:         if (seg.offset < 0 || seg.offset >= seg.array.length)
 383:           invalid = seg.offset;
 384:         else
 385:           invalid = seg.offset + seg.count;
 386:         throw new BadLocationException("Illegal location: array.length = "
 387:                                        + seg.array.length + ", offset = "
 388:                                        + seg.offset + ", count = "
 389:                                        + seg.count, invalid);
 390:       }
 391:   }
 392: 
 393:   /**
 394:    * Fetches a piece of content and stores it in a {@link Segment} object.
 395:    * 
 396:    * If the requested piece of text spans the gap, the content is copied into a
 397:    * new array. If it doesn't then it is contiguous and the actual content
 398:    * store is returned.
 399:    * 
 400:    * @param where the start location of the fragment
 401:    * @param len the length of the fragment
 402:    * @param txt the Segment object to store the fragment in
 403:    * 
 404:    * @throws BadLocationException if <code>where</code> or
 405:    *         <code>where + len</code> are no valid locations in the buffer
 406:    */
 407:   public void getChars(int where, int len, Segment txt)
 408:       throws BadLocationException
 409:   {
 410:     // check arguments
 411:     int length = length();
 412:     if (where < 0)
 413:       throw new BadLocationException("the where argument may not be below zero", where);
 414:     if (where >= length)
 415:       throw new BadLocationException("the where argument cannot be greater"
 416:           + " than the content length", where);
 417:     if ((where + len) > length)
 418:       throw new BadLocationException("len plus where cannot be greater"
 419:           + " than the content length", len + where);
 420: 
 421:     // check if requested segment is contiguous
 422:     if ((where < gapStart) && ((gapStart - where) < len))
 423:     {
 424:       // requested segment is not contiguous -> copy the pieces together
 425:       char[] copy = new char[len];
 426:       int lenFirst = gapStart - where; // the length of the first segment
 427:       System.arraycopy(buffer, where, copy, 0, lenFirst);
 428:       System.arraycopy(buffer, gapEnd, copy, lenFirst, len - lenFirst);
 429:       txt.array = copy;
 430:       txt.offset = 0;
 431:       txt.count = len;
 432:     }
 433:     else
 434:     {
 435:       // requested segment is contiguous -> we can simply return the
 436:       // actual content
 437:       txt.array = buffer;
 438:       if (where < gapStart)
 439:         txt.offset = where;
 440:       else
 441:         txt.offset = where + (gapEnd - gapStart);
 442:       txt.count = len;
 443:     }
 444:   }
 445: 
 446:   /**
 447:    * Creates and returns a mark at the specified position.
 448:    * 
 449:    * @param offset the position at which to create the mark
 450:    * 
 451:    * @return the create Position object for the mark
 452:    * 
 453:    * @throws BadLocationException if the offset is not a valid position in the
 454:    *         buffer
 455:    */
 456:   public Position createPosition(final int offset) throws BadLocationException
 457:   {
 458:     // We try to find a GapContentPosition at the specified offset and return
 459:     // that. Otherwise we must create a new one.
 460:     GapContentPosition pos = null;
 461:     Set positionSet = positions.keySet();
 462:     for (Iterator i = positionSet.iterator(); i.hasNext();)
 463:       {
 464:         GapContentPosition p = (GapContentPosition) i.next();
 465:         if (p.getOffset() == offset)
 466:           {
 467:             pos = p;
 468:             break;
 469:           }
 470:       }
 471: 
 472:     // If none was found, then create and return a new one.
 473:     if (pos == null)
 474:       {
 475:         int mark = offset;
 476:         if (mark >= gapStart)
 477:           mark += (gapEnd - gapStart);
 478:         pos = new GapContentPosition(mark);
 479:         positions.put(pos, null);
 480:       }
 481: 
 482:     return pos;
 483:   }
 484: 
 485:   /**
 486:    * Enlarges the gap. This allocates a new bigger buffer array, copy the
 487:    * segment before the gap as it is and the segment after the gap at the end
 488:    * of the new buffer array. This does change the gapEnd mark but not the
 489:    * gapStart mark.
 490:    * 
 491:    * @param newSize the new size of the gap
 492:    */
 493:   protected void shiftEnd(int newSize)
 494:   {
 495:     assert newSize > (gapEnd - gapStart) : "The new gap size must be greater "
 496:                                            + "than the old gap size";
 497: 
 498:     int delta = newSize - gapEnd + gapStart;
 499:     // Update the marks after the gapEnd.
 500:     adjustPositionsInRange(gapEnd, buffer.length - gapEnd, delta);
 501: 
 502:     // Copy the data around.
 503:     char[] newBuf = (char[]) allocateArray(length() + newSize);
 504:     System.arraycopy(buffer, 0, newBuf, 0, gapStart);
 505:     System.arraycopy(buffer, gapEnd, newBuf, gapStart + newSize, buffer.length
 506:         - gapEnd);
 507:     gapEnd = gapStart + newSize;
 508:     buffer = newBuf;
 509: 
 510:   }
 511: 
 512:   /**
 513:    * Shifts the gap to the specified position.
 514:    * 
 515:    * @param newGapStart the new start position of the gap
 516:    */
 517:   protected void shiftGap(int newGapStart)
 518:   {
 519:     if (newGapStart == gapStart)
 520:       return;
 521:     int newGapEnd = newGapStart + gapEnd - gapStart;
 522:     if (newGapStart < gapStart)
 523:       {
 524:         // Update the positions between newGapStart and (old) gapStart. The marks
 525:         // must be shifted by (gapEnd - gapStart).
 526:         adjustPositionsInRange(newGapStart, gapStart - newGapStart, gapEnd - gapStart);
 527:         System.arraycopy(buffer, newGapStart, buffer, newGapEnd, gapStart
 528:                          - newGapStart);
 529:         gapStart = newGapStart;
 530:         gapEnd = newGapEnd;
 531:       }
 532:     else
 533:       {
 534:         // Update the positions between newGapEnd and (old) gapEnd. The marks
 535:         // must be shifted by (gapEnd - gapStart).
 536:         adjustPositionsInRange(gapEnd, newGapEnd - gapEnd, -(gapEnd - gapStart));
 537:         System.arraycopy(buffer, gapEnd, buffer, gapStart, newGapStart
 538:                          - gapStart);
 539:         gapStart = newGapStart;
 540:         gapEnd = newGapEnd;
 541:       }
 542:     if (gapStart == 0)
 543:       resetMarksAtZero();
 544:   }
 545: 
 546:   /**
 547:    * Shifts the gap start downwards. This does not affect the content of the
 548:    * buffer. This only updates the gap start and all the marks that are between
 549:    * the old gap start and the new gap start. They all are squeezed to the start
 550:    * of the gap, because their location has been removed.
 551:    *
 552:    * @param newGapStart the new gap start
 553:    */
 554:   protected void shiftGapStartDown(int newGapStart)
 555:   {
 556:     if (newGapStart == gapStart)
 557:       return;
 558: 
 559:     assert newGapStart < gapStart : "The new gap start must be less than the "
 560:                                     + "old gap start.";
 561:     setPositionsInRange(newGapStart, gapStart, false);
 562:     gapStart = newGapStart;
 563:   }
 564: 
 565:   /**
 566:    * Shifts the gap end upwards. This does not affect the content of the
 567:    * buffer. This only updates the gap end and all the marks that are between
 568:    * the old gap end and the new end start. They all are squeezed to the end
 569:    * of the gap, because their location has been removed.
 570:    *
 571:    * @param newGapEnd the new gap start
 572:    */
 573:   protected void shiftGapEndUp(int newGapEnd)
 574:   {
 575:     if (newGapEnd == gapEnd)
 576:       return;
 577: 
 578:     assert newGapEnd > gapEnd : "The new gap end must be greater than the "
 579:                                 + "old gap end.";
 580:     setPositionsInRange(gapEnd, newGapEnd, false);
 581:     gapEnd = newGapEnd;
 582:   }
 583: 
 584:   /**
 585:    * Returns the allocated buffer array.
 586:    * 
 587:    * @return the allocated buffer array
 588:    */
 589:   protected final Object getArray()
 590:   {
 591:     return buffer;
 592:   }
 593: 
 594:   /**
 595:    * Replaces a portion of the storage with the specified items.
 596:    * 
 597:    * @param position the position at which to remove items
 598:    * @param rmSize the number of items to remove
 599:    * @param addItems the items to add at location
 600:    * @param addSize the number of items to add
 601:    */
 602:   protected void replace(int position, int rmSize, Object addItems,
 603:                          int addSize)
 604:   {
 605:     if (gapStart != position)
 606:       shiftGap(position);
 607:       
 608:     // Remove content
 609:     if (rmSize > 0) 
 610:       shiftGapEndUp(gapEnd + rmSize);
 611: 
 612:     // If gap is too small, enlarge the gap.
 613:     if ((gapEnd - gapStart) <= addSize)
 614:       shiftEnd((addSize - gapEnd + gapStart + 1) * 2 + gapEnd + DEFAULT_BUFSIZE);
 615: 
 616:     // Add new items to the buffer.
 617:     if (addItems != null)
 618:       {
 619:         System.arraycopy(addItems, 0, buffer, gapStart, addSize);
 620:         
 621:         
 622:         resetMarksAtZero();
 623:         
 624:         gapStart += addSize;
 625:       }
 626:   }
 627: 
 628:   /**
 629:    * Returns the start index of the gap within the buffer array.
 630:    *
 631:    * @return the start index of the gap within the buffer array
 632:    */
 633:   protected final int getGapStart()
 634:   {
 635:     return gapStart;
 636:   }
 637: 
 638:   /**
 639:    * Returns the end index of the gap within the buffer array.
 640:    *
 641:    * @return the end index of the gap within the buffer array
 642:    */
 643:   protected final int getGapEnd()
 644:   {
 645:     return gapEnd;
 646:   }
 647: 
 648:   /**
 649:    * Returns all <code>Position</code>s that are in the range specified by
 650:    * <code>offset</code> and </code>length</code> within the buffer array.
 651:    *
 652:    * @param v the vector to use; if <code>null</code>, a new Vector is allocated
 653:    * @param offset the start offset of the range to search
 654:    * @param length the length of the range to search
 655:    *
 656:    * @return the positions within the specified range
 657:    */
 658:   protected Vector getPositionsInRange(Vector v, int offset, int length)
 659:   {
 660:     Vector res = v;
 661:     if (res == null)
 662:       res = new Vector();
 663:     else
 664:       res.clear();
 665: 
 666:     int endOffs = offset + length;
 667: 
 668:     Set positionSet = positions.keySet();
 669:     for (Iterator i = positionSet.iterator(); i.hasNext();)
 670:       {
 671:         GapContentPosition p = (GapContentPosition) i.next();
 672:         int offs = p.getOffset();
 673:         if (offs >= offset && offs < endOffs)
 674:           res.add(p);
 675:       }
 676: 
 677:     return res;
 678:   }
 679:   
 680:   /**
 681:    * Crunches all positions in the specified range to either the start or
 682:    * end of that interval. The interval boundaries are meant to be inclusive
 683:    * [start, end].
 684:    *
 685:    * @param start the start offset of the range
 686:    * @param end the end offset of the range
 687:    * @param toStart a boolean indicating if the positions should be crunched
 688:    *        to the start (true) or to the end (false)
 689:    */
 690:   private void setPositionsInRange(int start, int end, boolean toStart)
 691:   {
 692:     // We slump together all the GapContentPositions to point to
 693:     // one mark. So this is implemented as follows:
 694:     // 1. Remove all the marks in the specified range.
 695:     // 2. Insert one new mark at the correct location.
 696:     // 3. Adjust all affected GapContentPosition instances to point to
 697:     //    this new mark.
 698: 
 699:     synchronized (this)
 700:       {
 701:         int startIndex = binarySearch(positionMarks, start, numMarks);
 702:         if (startIndex < 0) // Translate to insertion index, if not found.
 703:           startIndex = - startIndex - 1;
 704:         int endIndex = binarySearch(positionMarks, end, numMarks);
 705:         if (endIndex < 0) // Translate to insertion index - 1, if not found.
 706:           endIndex = - endIndex - 2;
 707: 
 708:         // Update the marks.
 709:         // We have inclusive interval bounds, but let one element over for
 710:         // filling in the new value.
 711:         int removed = endIndex - startIndex;
 712:         if (removed <= 0)
 713:           return;
 714:         System.arraycopy(positionMarks, endIndex + 1, positionMarks,
 715:                          startIndex + 1, positionMarks.length - endIndex - 1);
 716:         numMarks -= removed;
 717:         if (toStart)
 718:           {
 719:             positionMarks[startIndex] = start;
 720:           }
 721:         else
 722:           {
 723:             positionMarks[startIndex] = end;
 724:           }
 725: 
 726:         // Update all affected GapContentPositions to point to the new index
 727:         // and all GapContentPositions that come after the interval to
 728:         // have their index moved by -removed.
 729:         Set positionSet = positions.keySet();
 730:         for (Iterator i = positionSet.iterator(); i.hasNext();)
 731:           {
 732:             GapContentPosition p = (GapContentPosition) i.next();
 733:             if (p.index > startIndex || p.index <= endIndex)
 734:               p.index = startIndex;
 735:             else if (p.index > endIndex)
 736:               p.index -= removed;
 737:           }
 738:     }
 739:   }
 740:   
 741:   /**
 742:    * Adjusts the mark of all <code>Position</code>s that are in the range 
 743:    * specified by <code>offset</code> and </code>length</code> within 
 744:    * the buffer array by <code>increment</code>
 745:    *
 746:    * @param offset the start offset of the range to search
 747:    * @param length the length of the range to search
 748:    * @param incr the increment
 749:    */
 750:   private void adjustPositionsInRange(int offset, int length, int incr)
 751:   {
 752:     int endMark = offset + length;
 753: 
 754:     synchronized (this)
 755:       {
 756:         // Find the start and end indices in the positionMarks array.
 757:         int startIndex = binarySearch(positionMarks, offset, numMarks);
 758:         if (startIndex < 0) // Translate to insertion index, if not found.
 759:           startIndex = - startIndex - 1;
 760:         int endIndex = binarySearch(positionMarks, endMark, numMarks);
 761:         if (endIndex < 0) // Translate to insertion index - 1, if not found.
 762:           endIndex = - endIndex - 2;
 763: 
 764:         // We must not change the order of the marks, this would have
 765:         // unpredictable results while binary-searching the marks.
 766:         assert (startIndex <= 0
 767:                 || positionMarks[startIndex - 1]
 768:                                  <= positionMarks [startIndex] + incr)
 769:                && (endIndex >= numMarks - 1
 770:                    || positionMarks[endIndex + 1]
 771:                                     >= positionMarks[endIndex] + incr)
 772:                 : "Adjusting the marks must not change their order";
 773: 
 774:         // Some debug helper output to determine if the start or end of the
 775:         // should ever be coalesced together with adjecent marks.
 776:         if (startIndex > 0 && positionMarks[startIndex - 1]
 777:                                           == positionMarks[startIndex] + incr)
 778:           System.err.println("DEBUG: We could coalesce the start of the region"
 779:                              + " in GapContent.adjustPositionsInRange()");
 780:         if (endIndex < numMarks - 1 && positionMarks[endIndex + 1]
 781:                                             == positionMarks[endIndex] + incr)
 782:             System.err.println("DEBUG: We could coalesce the end of the region"
 783:                                + " in GapContent.adjustPositionsInRange()");
 784: 
 785:         // Actually adjust the marks.
 786:         for (int i = startIndex; i <= endIndex; i++)
 787:           positionMarks[i] += incr;
 788:       }
 789: 
 790:   }
 791: 
 792:   /**
 793:    * Resets all <code>Position</code> that have an offset of <code>0</code>,
 794:    * to also have an array index of <code>0</code>. This might be necessary
 795:    * after a call to <code>shiftGap(0)</code>, since then the marks at offset
 796:    * <code>0</code> get shifted to <code>gapEnd</code>.
 797:    */
 798:   protected void resetMarksAtZero()
 799:   {
 800:     if (gapStart != 0)
 801:       return;
 802: 
 803:     positionMarks[0] = 0;
 804:   }
 805: 
 806:   /**
 807:    * @specnote This method is not very well specified and the positions vector
 808:    *           is implementation specific. The undo positions are managed
 809:    *           differently in this implementation, this method is only here
 810:    *           for binary compatibility.
 811:    */
 812:   protected void updateUndoPositions(Vector positions, int offset, int length)
 813:   {
 814:     // We do nothing here.
 815:   }
 816: 
 817:   /**
 818:    * Outputs debugging info to System.err. It prints out the buffer array,
 819:    * the gapStart is marked by a &lt; sign, the gapEnd is marked by a &gt;
 820:    * sign and each position is marked by a # sign.
 821:    */
 822:   private void dump()
 823:   {
 824:     System.err.println("GapContent debug information");
 825:     System.err.println("buffer length: " + buffer.length);
 826:     System.err.println("gap start: " + gapStart);
 827:     System.err.println("gap end: " + gapEnd);
 828:     for (int i = 0; i < buffer.length; i++)
 829:       {
 830:         if (i == gapStart)
 831:           System.err.print('<');
 832:         if (i == gapEnd)
 833:           System.err.print('>');
 834: 
 835:         if (!Character.isISOControl(buffer[i]))
 836:           System.err.print(buffer[i]);
 837:         else
 838:           System.err.print('.');
 839:       }
 840:     System.err.println();
 841:   }
 842: 
 843:   /**
 844:    * Prints out the position marks.
 845:    */
 846:   private void dumpMarks()
 847:   {
 848:     System.err.print("positionMarks: ");
 849:     for (int i = 0; i < numMarks; i++)
 850:       System.err.print(positionMarks[i] + ", ");
 851:     System.err.println();
 852:   }
 853: 
 854:   /**
 855:    * Inserts a mark into the positionMarks array. This must update all the
 856:    * GapContentPosition instances in positions that come after insertionPoint.
 857:    *
 858:    * This is package private to avoid synthetic accessor methods.
 859:    *
 860:    * @param insertionPoint the index at which to insert the mark
 861:    * @param mark the mark to insert
 862:    */
 863:   void insertMark(int insertionPoint, int mark)
 864:   {
 865:     synchronized (this)
 866:       {
 867:         // Update the positions.
 868:         Set positionSet = positions.keySet();
 869:         for (Iterator i = positionSet.iterator(); i.hasNext();)
 870:           {
 871:             GapContentPosition p = (GapContentPosition) i.next();
 872:             if (p.index >= insertionPoint)
 873:               p.index++;
 874:           }
 875: 
 876:         // Update the position marks.
 877:         if (positionMarks.length <= numMarks)
 878:           {
 879:             int[] newMarks = new int[positionMarks.length + 10];
 880:             System.arraycopy(positionMarks, 0, newMarks, 0, insertionPoint);
 881:             newMarks[insertionPoint] = mark;
 882:             System.arraycopy(positionMarks, insertionPoint, newMarks,
 883:                              insertionPoint + 1,
 884:                              numMarks - insertionPoint);
 885:             positionMarks = newMarks;
 886:           }
 887:         else
 888:           {
 889:             System.arraycopy(positionMarks, insertionPoint, positionMarks,
 890:                              insertionPoint + 1,
 891:                              numMarks - insertionPoint);
 892:             positionMarks[insertionPoint] = mark;
 893:           }
 894:         numMarks++;
 895:       }
 896:   }
 897: 
 898:   /**
 899:    * An adaption of {@link java.util.Arrays#binarySearch(int[], int)} to 
 900:    * specify a maximum index up to which the array is searched. This allows
 901:    * us to have some trailing entries that we ignore.
 902:    *
 903:    * This is package private to avoid synthetic accessor methods.
 904:    *
 905:    * @param a the array
 906:    * @param key the key to search for
 907:    * @param maxIndex the maximum index up to which the search is performed
 908:    *
 909:    * @return the index of the found entry, or (-(index)-1) for the
 910:    *         insertion point when not found
 911:    *
 912:    * @see java.util.Arrays#binarySearch(int[], int)
 913:    */
 914:   int binarySearch(int[] a, int key, int maxIndex)
 915:   {
 916:     int low = 0;
 917:     int hi = maxIndex - 1;
 918:     int mid = 0;
 919:     while (low <= hi)
 920:       {
 921:         mid = (low + hi) >>> 1;
 922:         final int d = a[mid];
 923:         if (d == key)
 924:           return mid;
 925:         else if (d > key)
 926:           hi = mid - 1;
 927:         else
 928:           // This gets the insertion point right on the last loop.
 929:           low = ++mid;
 930:       }
 931:     return -mid - 1;
 932:   }
 933: }