bugfix 1423269, http://sourceforge.net/tracker/index.php?func=detail&aid=1423269...
[phpeclipse.git] / net.sourceforge.phpeclipse / src / net / sourceforge / phpeclipse / phpeditor / PaintManager.java
1 package net.sourceforge.phpeclipse.phpeditor;
2
3
4 /*
5  * (c) Copyright IBM Corp. 2000, 2001.
6  * All Rights Reserved.
7  */
8
9 import java.util.ArrayList;
10 import java.util.Iterator;
11 import java.util.List;
12
13 import org.eclipse.jface.text.BadLocationException;
14 import org.eclipse.jface.text.BadPositionCategoryException;
15 import org.eclipse.jface.text.DefaultPositionUpdater;
16 import org.eclipse.jface.text.IDocument;
17 import org.eclipse.jface.text.IPositionUpdater;
18 import org.eclipse.jface.text.ITextInputListener;
19 import org.eclipse.jface.text.ITextListener;
20 import org.eclipse.jface.text.Position;
21 import org.eclipse.jface.text.TextEvent;
22 import org.eclipse.jface.text.source.ISourceViewer;
23 import org.eclipse.jface.viewers.ISelectionChangedListener;
24 import org.eclipse.jface.viewers.ISelectionProvider;
25 import org.eclipse.jface.viewers.SelectionChangedEvent;
26 import org.eclipse.swt.custom.StyledText;
27 import org.eclipse.swt.events.KeyEvent;
28 import org.eclipse.swt.events.KeyListener;
29 import org.eclipse.swt.events.MouseEvent;
30 import org.eclipse.swt.events.MouseListener;
31 import org.eclipse.swt.widgets.Control;
32
33
34 public final class PaintManager implements KeyListener, MouseListener, ISelectionChangedListener, ITextListener, ITextInputListener {           
35                                         
36
37         static class PaintPositionUpdater extends DefaultPositionUpdater {
38                 
39                 /**
40                  * Creates the position updater.
41                  */
42                 protected PaintPositionUpdater(String category) {
43                         super(category);
44                 }
45                 
46                 /**
47                  * If an insertion happens at a position's offset, the
48                  * position is extended rather than shifted. Also, if something is added 
49                  * right behind the end of the position, the position is extended rather
50                  * than kept stable.
51                  */
52                 protected void adaptToInsert() {
53                         
54                         int myStart= fPosition.offset;
55                         int myEnd=   fPosition.offset + fPosition.length;
56                         myEnd= Math.max(myStart, myEnd);
57                         
58                         int yoursStart= fOffset;
59                         int yoursEnd=   fOffset + fReplaceLength;// - 1;
60                         yoursEnd= Math.max(yoursStart, yoursEnd);
61                         
62                         if (myEnd < yoursStart)
63                                 return;
64                         
65                         if (myStart <= yoursStart)
66                                 fPosition.length += fReplaceLength;
67                         else
68                                 fPosition.offset += fReplaceLength;
69                 }
70         };
71
72         static class PositionManager implements IPositionManager {
73                 
74                 private IDocument fDocument;
75                 private IPositionUpdater fPositionUpdater;
76                 private String fCategory;
77                 
78                 public PositionManager() {
79                         fCategory= getClass().getName() + hashCode();
80                         fPositionUpdater= new PaintPositionUpdater(fCategory);
81                 }
82
83                 public void install(IDocument document) {
84                         fDocument= document;
85                         fDocument.addPositionCategory(fCategory);
86                         fDocument.addPositionUpdater(fPositionUpdater);
87                 }
88                 
89                 public void dispose() {
90                         uninstall(fDocument);
91                 }
92                 
93                 public void uninstall(IDocument document) {
94                         if (document == fDocument && document != null) {
95                                 try {
96                                         fDocument.removePositionUpdater(fPositionUpdater);
97                                         fDocument.removePositionCategory(fCategory);                    
98                                 } catch (BadPositionCategoryException x) {
99                                         // should not happen
100                                 }
101                                 fDocument= null;
102                         }
103                 }
104                 
105                 /*
106                  * @see IPositionManager#addManagedPosition(Position)
107                  */
108                 public void addManagedPosition(Position position) {
109                         try {
110                                 fDocument.addPosition(fCategory, position);
111                         } catch (BadPositionCategoryException x) {
112                                 // should not happen
113                         } catch (BadLocationException x) {
114                                 // should not happen
115                         }
116                 }
117                 
118                 /*
119                  * @see IPositionManager#removeManagedPosition(Position)
120                  */
121                 public void removeManagedPosition(Position position) {
122                         try {
123                                 fDocument.removePosition(fCategory, position);
124                         } catch (BadPositionCategoryException x) {
125                                 // should not happen
126                         }
127                 }
128         };
129         
130         
131         private List fPainters= new ArrayList(2);
132         private PositionManager fManager;
133         private ISourceViewer fSourceViewer;
134         private boolean fTextChanged= false;
135         private boolean fAutoRepeat= false;
136         
137         
138         public PaintManager(ISourceViewer sourceViewer) {
139                 fSourceViewer= sourceViewer;
140         }
141         
142         public void addPainter(IPainter painter) {
143                 if (!fPainters.contains(painter)) {
144                         fPainters.add(painter);
145                         if (fPainters.size() == 1)
146                                 install();
147                         painter.setPositionManager(fManager);
148                         painter.paint(IPainter.INTERNAL);
149                 }
150         }
151         
152         public void removePainter(IPainter painter) {
153                 if (fPainters.remove(painter))
154                         painter.setPositionManager(null);
155                 if (fPainters.size() == 0)
156                         dispose();
157         }
158         
159         private void install() {
160                 
161                 fManager= new PositionManager();
162                 fManager.install(fSourceViewer.getDocument());
163                 
164                 fSourceViewer.addTextInputListener(this);
165                 
166                 ISelectionProvider provider= fSourceViewer.getSelectionProvider();
167                 provider.addSelectionChangedListener(this);
168                 
169                 fSourceViewer.addTextListener(this);
170                 
171                 StyledText text= fSourceViewer.getTextWidget();
172                 text.addKeyListener(this);
173                 text.addMouseListener(this);
174         }
175         
176         public void dispose() {
177                 
178                 if (fManager != null) {
179                         fManager.dispose();
180                         fManager= null;
181                 }
182                 
183                 for (Iterator e = fPainters.iterator(); e.hasNext();)
184                         ((IPainter) e.next()).dispose();        
185                 fPainters.clear();
186                 
187                 fSourceViewer.removeTextInputListener(this);
188                 
189                 ISelectionProvider provider= fSourceViewer.getSelectionProvider();
190                 if (provider != null)
191                         provider.removeSelectionChangedListener(this);
192                 
193                 fSourceViewer.removeTextListener(this);
194                 
195                 StyledText text= fSourceViewer.getTextWidget();
196                 if (text != null && !text.isDisposed()) {
197                         text.removeKeyListener(this);
198                         text.removeMouseListener(this);
199                 }
200         }
201         
202         private void paint(int reason) {
203                 for (Iterator e = fPainters.iterator(); e.hasNext();)
204                         ((IPainter) e.next()).paint(reason);
205         }
206         
207         /*
208          * @see KeyListener#keyPressed(KeyEvent)
209          */
210         public void keyPressed(KeyEvent e) {
211                 paint(IPainter.KEY_STROKE);
212         }
213
214         /*
215          * @see KeyListener#keyReleased(KeyEvent)
216          */
217         public void keyReleased(KeyEvent e) {
218         }
219
220         /*
221          * @see MouseListener#mouseDoubleClick(MouseEvent)
222          */
223         public void mouseDoubleClick(MouseEvent e) {
224         }
225         
226         /*
227          * @see MouseListener#mouseDown(MouseEvent)
228          */
229         public void mouseDown(MouseEvent e) {
230                 paint(IPainter.MOUSE_BUTTON);
231         }
232         
233         /*
234          * @see MouseListener#mouseUp(MouseEvent)
235          */
236         public void mouseUp(MouseEvent e) {
237         }
238         
239         /*
240          * @see ISelectionChangedListener#selectionChanged(SelectionChangedEvent)
241          */
242         public void selectionChanged(SelectionChangedEvent event) {
243                 paint(IPainter.SELECTION);
244         }
245         
246         /*
247          * @see ITextListener#textChanged(TextEvent)
248          */
249         public void textChanged(TextEvent event) {
250                 
251                 if (!event.getViewerRedrawState())
252                         return;
253                         
254                 fTextChanged= true;
255                 Control control= fSourceViewer.getTextWidget();
256                 if (control != null) {
257                         control.getDisplay().asyncExec(new Runnable() {
258                                 public void run() {
259                                         if (fTextChanged && fSourceViewer != null) 
260                                                 paint(IPainter.TEXT_CHANGE);
261                                 }
262                         });
263                 }
264         }
265         
266         /*
267          * @see ITextInputListener#inputDocumentAboutToBeChanged(IDocument, IDocument)
268          */
269         public void inputDocumentAboutToBeChanged(IDocument oldInput, IDocument newInput) {
270                 if (oldInput != null) {
271                         for (Iterator e = fPainters.iterator(); e.hasNext();)
272                                 ((IPainter) e.next()).deactivate(false);                                
273                         fManager.uninstall(oldInput);
274                 }
275         }
276         
277         /*
278          * @see ITextInputListener#inputDocumentChanged(IDocument, IDocument)
279          */
280         public void inputDocumentChanged(IDocument oldInput, IDocument newInput) {
281                 if (newInput != null) {
282                         fManager.install(newInput);
283                         paint(IPainter.TEXT_CHANGE);
284                 }
285         }
286 }
287