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