001: /*
002: * PositionManager.java - Manages positions
003: * :tabSize=8:indentSize=8:noTabs=false:
004: * :folding=explicit:collapseFolds=1:
005: *
006: * Copyright (C) 2001, 2005 Slava Pestov
007: *
008: * This program is free software; you can redistribute it and/or
009: * modify it under the terms of the GNU General Public License
010: * as published by the Free Software Foundation; either version 2
011: * of the License, or any later version.
012: *
013: * This program is distributed in the hope that it will be useful,
014: * but WITHOUT ANY WARRANTY; without even the implied warranty of
015: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
016: * GNU General Public License for more details.
017: *
018: * You should have received a copy of the GNU General Public License
019: * along with this program; if not, write to the Free Software
020: * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
021: */
022:
023: package org.gjt.sp.jedit.buffer;
024:
025: //{{{ Imports
026: import javax.swing.text.Position;
027: import java.util.*;
028: import org.gjt.sp.util.Log;
029:
030: //}}}
031:
032: /**
033: * A class internal to jEdit's document model. You should not use it
034: * directly.
035: *
036: * @author Slava Pestov
037: * @version $Id: PositionManager.java 9007 2007-02-22 10:35:38Z kpouer $
038: * @since jEdit 4.2pre3
039: */
040: public class PositionManager {
041: //{{{ PositionManager constructor
042: public PositionManager(JEditBuffer buffer) {
043: this .buffer = buffer;
044: } //}}}
045:
046: //{{{ createPosition() method
047: public synchronized Position createPosition(int offset) {
048: PosBottomHalf bh = new PosBottomHalf(offset);
049: PosBottomHalf existing = positions.get(bh);
050: if (existing == null) {
051: positions.put(bh, bh);
052: existing = bh;
053: }
054:
055: return new PosTopHalf(existing);
056: } //}}}
057:
058: //{{{ contentInserted() method
059: public synchronized void contentInserted(int offset, int length) {
060: if (positions.isEmpty())
061: return;
062:
063: /* get all positions from offset to the end, inclusive */
064: Iterator iter = positions.tailMap(new PosBottomHalf(offset))
065: .keySet().iterator();
066:
067: iteration = true;
068: while (iter.hasNext()) {
069: ((PosBottomHalf) iter.next()).contentInserted(offset,
070: length);
071: }
072: iteration = false;
073: } //}}}
074:
075: //{{{ contentRemoved() method
076: public synchronized void contentRemoved(int offset, int length) {
077: if (positions.isEmpty())
078: return;
079:
080: /* get all positions from offset to the end, inclusive */
081: Iterator iter = positions.tailMap(new PosBottomHalf(offset))
082: .keySet().iterator();
083:
084: iteration = true;
085: while (iter.hasNext()) {
086: ((PosBottomHalf) iter.next())
087: .contentRemoved(offset, length);
088: }
089: iteration = false;
090:
091: } //}}}
092:
093: boolean iteration;
094:
095: //{{{ Private members
096: private JEditBuffer buffer;
097: private SortedMap<PosBottomHalf, PosBottomHalf> positions = new TreeMap<PosBottomHalf, PosBottomHalf>();
098:
099: //}}}
100:
101: //{{{ Inner classes
102:
103: //{{{ PosTopHalf class
104: class PosTopHalf implements Position {
105: PosBottomHalf bh;
106:
107: //{{{ PosTopHalf constructor
108: PosTopHalf(PosBottomHalf bh) {
109: this .bh = bh;
110: bh.ref();
111: } //}}}
112:
113: //{{{ getOffset() method
114: public int getOffset() {
115: return bh.offset;
116: } //}}}
117:
118: //{{{ finalize() method
119: protected void finalize() {
120: synchronized (PositionManager.this ) {
121: bh.unref();
122: }
123: } //}}}
124: } //}}}
125:
126: //{{{ PosBottomHalf class
127: class PosBottomHalf implements Comparable<PosBottomHalf> {
128: int offset;
129: int ref;
130:
131: //{{{ PosBottomHalf constructor
132: PosBottomHalf(int offset) {
133: this .offset = offset;
134: } //}}}
135:
136: //{{{ ref() method
137: void ref() {
138: ref++;
139: } //}}}
140:
141: //{{{ unref() method
142: void unref() {
143: if (--ref == 0)
144: positions.remove(this );
145: } //}}}
146:
147: //{{{ contentInserted() method
148: void contentInserted(int offset, int length) {
149: if (offset > this .offset)
150: throw new ArrayIndexOutOfBoundsException();
151: this .offset += length;
152: checkInvariants();
153: } //}}}
154:
155: //{{{ contentRemoved() method
156: void contentRemoved(int offset, int length) {
157: if (offset > this .offset)
158: throw new ArrayIndexOutOfBoundsException();
159: if (this .offset <= offset + length)
160: this .offset = offset;
161: else
162: this .offset -= length;
163: checkInvariants();
164: } //}}}
165:
166: //{{{ equals() method
167: public boolean equals(Object o) {
168: if (!(o instanceof PosBottomHalf))
169: return false;
170:
171: return ((PosBottomHalf) o).offset == offset;
172: } //}}}
173:
174: //{{{ compareTo() method
175: public int compareTo(PosBottomHalf posBottomHalf) {
176: if (iteration)
177: Log.log(Log.ERROR, this , "Consistency failure");
178: return offset - posBottomHalf.offset;
179: } //}}}
180:
181: //{{{ checkInvariants() method
182: private void checkInvariants() {
183: if (offset < 0 || offset > buffer.getLength())
184: throw new ArrayIndexOutOfBoundsException();
185: } //}}}
186: } //}}}
187:
188: //}}}
189: }
|