349 return rec.offset;
350 }
351
352 protected void finalize() throws Throwable {
353 // schedule the record to be removed later
354 // on another thread.
355 rec.unused = true;
356 }
357
358 public String toString() {
359 return Integer.toString(getOffset());
360 }
361
362 PosRec rec;
363 }
364
365 /**
366 * Used to hold a reference to a Position that is being reset as the
367 * result of removing from the content.
368 */
369 final class UndoPosRef {
370 UndoPosRef(PosRec rec) {
371 this.rec = rec;
372 this.undoLocation = rec.offset;
373 }
374
375 /**
376 * Resets the location of the Position to the offset when the
377 * receiver was instantiated.
378 */
379 protected void resetLocation() {
380 rec.offset = undoLocation;
381 }
382
383 /** Location to reset to when resetLocatino is invoked. */
384 protected int undoLocation;
385 /** Position to reset offset. */
386 protected PosRec rec;
387 }
388
389 /**
390 * UnoableEdit created for inserts.
391 */
392 class InsertUndo extends AbstractUndoableEdit {
393 protected InsertUndo(int offset, int length) {
394 super();
395 this.offset = offset;
396 this.length = length;
397 }
398
399 public void undo() throws CannotUndoException {
400 super.undo();
401 try {
402 synchronized(StringContent.this) {
403 // Get the Positions in the range being removed.
404 if(marks != null)
405 posRefs = getPositionsInRange(null, offset, length);
406 string = getString(offset, length);
|
349 return rec.offset;
350 }
351
352 protected void finalize() throws Throwable {
353 // schedule the record to be removed later
354 // on another thread.
355 rec.unused = true;
356 }
357
358 public String toString() {
359 return Integer.toString(getOffset());
360 }
361
362 PosRec rec;
363 }
364
365 /**
366 * Used to hold a reference to a Position that is being reset as the
367 * result of removing from the content.
368 */
369 protected final class UndoPosRef {
370 UndoPosRef(PosRec rec) {
371 this.rec = rec;
372 this.undoLocation = rec.offset;
373 }
374
375 /**
376 * Resets the location of the Position to the offset when the
377 * receiver was instantiated.
378 */
379 void resetLocation() {
380 rec.offset = undoLocation;
381 }
382
383 /** Location to reset to when resetLocatino is invoked. */
384 private int undoLocation;
385 /** Position to reset offset. */
386 private PosRec rec;
387 }
388
389 /**
390 * UnoableEdit created for inserts.
391 */
392 class InsertUndo extends AbstractUndoableEdit {
393 protected InsertUndo(int offset, int length) {
394 super();
395 this.offset = offset;
396 this.length = length;
397 }
398
399 public void undo() throws CannotUndoException {
400 super.undo();
401 try {
402 synchronized(StringContent.this) {
403 // Get the Positions in the range being removed.
404 if(marks != null)
405 posRefs = getPositionsInRange(null, offset, length);
406 string = getString(offset, length);
|