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