Source code: org/gjt/sp/jedit/buffer/PositionManager.java
1 /*
2 * PositionManager.java - Manages positions
3 * :tabSize=8:indentSize=8:noTabs=false:
4 * :folding=explicit:collapseFolds=1:
5 *
6 * Copyright (C) 2001, 2003 Slava Pestov
7 *
8 * This program is free software; you can redistribute it and/or
9 * modify it under the terms of the GNU General Public License
10 * as published by the Free Software Foundation; either version 2
11 * of the License, or any later version.
12 *
13 * This program is distributed in the hope that it will be useful,
14 * but WITHOUT ANY WARRANTY; without even the implied warranty of
15 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
16 * GNU General Public License for more details.
17 *
18 * You should have received a copy of the GNU General Public License
19 * along with this program; if not, write to the Free Software
20 * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
21 */
22
23 package org.gjt.sp.jedit.buffer;
24
25 //{{{ Imports
26 import javax.swing.text.Position;
27 import java.util.*;
28 import org.gjt.sp.util.Log;
29 //}}}
30
31 /**
32 * A class internal to jEdit's document model. You should not use it
33 * directly.
34 *
35 * @author Slava Pestov
36 * @version $Id: PositionManager.java,v 1.35 2003/11/18 20:51:57 spestov Exp $
37 * @since jEdit 4.2pre3
38 */
39 public class PositionManager
40 {
41 //{{{ createPosition() method
42 public synchronized Position createPosition(int offset)
43 {
44 PosBottomHalf bh = new PosBottomHalf(offset);
45 PosBottomHalf existing = (PosBottomHalf)positions.get(bh);
46 if(existing == null)
47 {
48 positions.put(bh,bh);
49 existing = bh;
50 }
51
52 return new PosTopHalf(existing);
53 } //}}}
54
55 //{{{ contentInserted() method
56 public synchronized void contentInserted(int offset, int length)
57 {
58 if(positions.size() == 0)
59 return;
60
61 /* get all positions from offset to the end, inclusive */
62 Iterator iter = positions.tailMap(new PosBottomHalf(offset))
63 .keySet().iterator();
64
65 iteration = true;
66 while(iter.hasNext())
67 {
68 PosBottomHalf bh = (PosBottomHalf)iter.next();
69 bh.offset += length;
70 }
71 iteration = false;
72 } //}}}
73
74 //{{{ contentRemoved() method
75 public synchronized void contentRemoved(int offset, int length)
76 {
77 if(positions.size() == 0)
78 return;
79
80 /* get all positions from offset to the end, inclusive */
81 Iterator iter = positions.tailMap(new PosBottomHalf(offset))
82 .keySet().iterator();
83
84 iteration = true;
85 while(iter.hasNext())
86 {
87 PosBottomHalf bh = (PosBottomHalf)iter.next();
88 if(bh.offset <= offset + length)
89 bh.offset = offset;
90 else
91 bh.offset -= length;
92 }
93 iteration = false;
94
95 } //}}}
96
97 boolean iteration;
98
99 //{{{ Private members
100 private SortedMap positions = new TreeMap();
101 //}}}
102
103 //{{{ Inner classes
104
105 //{{{ PosTopHalf class
106 class PosTopHalf implements Position
107 {
108 PosBottomHalf bh;
109
110 //{{{ PosTopHalf constructor
111 PosTopHalf(PosBottomHalf bh)
112 {
113 this.bh = bh;
114 bh.ref();
115 } //}}}
116
117 //{{{ getOffset() method
118 public int getOffset()
119 {
120 return bh.offset;
121 } //}}}
122
123 //{{{ finalize() method
124 protected void finalize()
125 {
126 synchronized(PositionManager.this)
127 {
128 bh.unref();
129 }
130 } //}}}
131 } //}}}
132
133 //{{{ PosBottomHalf class
134 class PosBottomHalf implements Comparable
135 {
136 int offset;
137 int ref;
138
139 //{{{ PosBottomHalf constructor
140 PosBottomHalf(int offset)
141 {
142 this.offset = offset;
143 } //}}}
144
145 //{{{ ref() method
146 void ref()
147 {
148 ref++;
149 } //}}}
150
151 //{{{ unref() method
152 void unref()
153 {
154 if(--ref == 0)
155 positions.remove(this);
156 } //}}}
157
158 //{{{ equals() method
159 public boolean equals(Object o)
160 {
161 if(!(o instanceof PosBottomHalf))
162 return false;
163
164 return ((PosBottomHalf)o).offset == offset;
165 } //}}}
166
167 //{{{ compareTo() method
168 public int compareTo(Object o)
169 {
170 if(iteration)
171 Log.log(Log.ERROR,this,"Consistency failure");
172 return offset - ((PosBottomHalf)o).offset;
173 } //}}}
174 } //}}}
175
176 //}}}
177 }