net.sourceforge.phpeclipse/src/net/sourceforge/phpeclipse/phpeditor/PaintManager.java

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