diff options
Diffstat (limited to 'org.eclipse.ui.console/src/org/eclipse/ui/console/TextConsoleViewer.java')
| -rw-r--r-- | org.eclipse.ui.console/src/org/eclipse/ui/console/TextConsoleViewer.java | 1142 |
1 files changed, 571 insertions, 571 deletions
diff --git a/org.eclipse.ui.console/src/org/eclipse/ui/console/TextConsoleViewer.java b/org.eclipse.ui.console/src/org/eclipse/ui/console/TextConsoleViewer.java index fe5b069af..0b28a96e1 100644 --- a/org.eclipse.ui.console/src/org/eclipse/ui/console/TextConsoleViewer.java +++ b/org.eclipse.ui.console/src/org/eclipse/ui/console/TextConsoleViewer.java @@ -74,64 +74,64 @@ import org.eclipse.ui.progress.WorkbenchJob; * @since 3.1 */ public class TextConsoleViewer extends SourceViewer implements LineStyleListener, LineBackgroundListener, MouseTrackListener, MouseMoveListener, MouseListener { - /** - * Adapts document to the text widget. - */ - private ConsoleDocumentAdapter documentAdapter; + /** + * Adapts document to the text widget. + */ + private ConsoleDocumentAdapter documentAdapter; - private IHyperlink hyperlink; + private IHyperlink hyperlink; - private Cursor handCursor; + private Cursor handCursor; - private Cursor textCursor; + private Cursor textCursor; - private int consoleWidth = -1; + private int consoleWidth = -1; - private TextConsole console; + private TextConsole console; - private IPropertyChangeListener propertyChangeListener; + private IPropertyChangeListener propertyChangeListener; private IScrollLockStateProvider scrollLockStateProvider; - private IDocumentListener documentListener = new IDocumentListener() { - @Override + private IDocumentListener documentListener = new IDocumentListener() { + @Override public void documentAboutToBeChanged(DocumentEvent event) { - } + } - @Override + @Override public void documentChanged(DocumentEvent event) { - updateLinks(event.fOffset); - } - }; - // event listener used to send event to hyperlink for IHyperlink2 - private Listener mouseUpListener = new Listener() { + updateLinks(event.fOffset); + } + }; + // event listener used to send event to hyperlink for IHyperlink2 + private Listener mouseUpListener = new Listener() { @Override public void handleEvent(Event event) { - if (hyperlink != null) { - String selection = getTextWidget().getSelectionText(); - if (selection.length() <= 0) { - if (event.button == 1) { - if (hyperlink instanceof IHyperlink2) { + if (hyperlink != null) { + String selection = getTextWidget().getSelectionText(); + if (selection.length() <= 0) { + if (event.button == 1) { + if (hyperlink instanceof IHyperlink2) { ((IHyperlink2) hyperlink).linkActivated(event); } else { hyperlink.linkActivated(); } - } - } - } + } + } + } } }; // to store to user scroll lock action private AtomicBoolean userHoldsScrollLock = new AtomicBoolean(false); - WorkbenchJob revealJob = new WorkbenchJob("Reveal End of Document") {//$NON-NLS-1$ - @Override + WorkbenchJob revealJob = new WorkbenchJob("Reveal End of Document") {//$NON-NLS-1$ + @Override public IStatus runInUIThread(IProgressMonitor monitor) { scrollToEndOfDocument(); - return Status.OK_STATUS; - } - }; + return Status.OK_STATUS; + } + }; // reveal the end of the document private void scrollToEndOfDocument() { @@ -171,29 +171,29 @@ public class TextConsoleViewer extends SourceViewer implements LineStyleListener return false; } - private IPositionUpdater positionUpdater = new IPositionUpdater() { - @Override + private IPositionUpdater positionUpdater = new IPositionUpdater() { + @Override public void update(DocumentEvent event) { - try { - IDocument document = getDocument(); - if (document != null) { - Position[] positions = document.getPositions(ConsoleHyperlinkPosition.HYPER_LINK_CATEGORY); - for (int i = 0; i < positions.length; i++) { - Position position = positions[i]; - if (position.offset == event.fOffset && position.length<=event.fLength) { - position.delete(); - } - if (position.isDeleted) { - document.removePosition(ConsoleHyperlinkPosition.HYPER_LINK_CATEGORY, position); - } - } - } - } catch (BadPositionCategoryException e) { - } - } - }; - - /** + try { + IDocument document = getDocument(); + if (document != null) { + Position[] positions = document.getPositions(ConsoleHyperlinkPosition.HYPER_LINK_CATEGORY); + for (int i = 0; i < positions.length; i++) { + Position position = positions[i]; + if (position.offset == event.fOffset && position.length<=event.fLength) { + position.delete(); + } + if (position.isDeleted) { + document.removePosition(ConsoleHyperlinkPosition.HYPER_LINK_CATEGORY, position); + } + } + } + } catch (BadPositionCategoryException e) { + } + } + }; + + /** * Constructs a new viewer in the given parent for the specified console. * * @param parent the containing composite @@ -214,22 +214,22 @@ public class TextConsoleViewer extends SourceViewer implements LineStyleListener * @param parent containing widget * @param console text console */ - public TextConsoleViewer(Composite parent, TextConsole console) { - super(parent, null, SWT.V_SCROLL | SWT.H_SCROLL); - this.console = console; - - IDocument document = console.getDocument(); - setDocument(document); - - StyledText styledText = getTextWidget(); - styledText.setDoubleClickEnabled(true); - styledText.addLineStyleListener(this); - styledText.addLineBackgroundListener(this); - styledText.setEditable(true); - styledText.setBackground(console.getBackground()); - setFont(console.getFont()); - styledText.addMouseTrackListener(this); - styledText.addListener(SWT.MouseUp, mouseUpListener); + public TextConsoleViewer(Composite parent, TextConsole console) { + super(parent, null, SWT.V_SCROLL | SWT.H_SCROLL); + this.console = console; + + IDocument document = console.getDocument(); + setDocument(document); + + StyledText styledText = getTextWidget(); + styledText.setDoubleClickEnabled(true); + styledText.addLineStyleListener(this); + styledText.addLineBackgroundListener(this); + styledText.setEditable(true); + styledText.setBackground(console.getBackground()); + setFont(console.getFont()); + styledText.addMouseTrackListener(this); + styledText.addListener(SWT.MouseUp, mouseUpListener); // event listener used to send event to vertical scroll bar styledText.getVerticalBar().addSelectionListener(new SelectionAdapter() { @Override @@ -277,7 +277,7 @@ public class TextConsoleViewer extends SourceViewer implements LineStyleListener } else if (e.keyCode == SWT.END || e.keyCode == SWT.BOTTOM) { setScrollLock(false);// selecting END makes it reveal the - // end + // end } else if ((e.keyCode == SWT.PAGE_DOWN || e.keyCode == SWT.ARROW_DOWN) && checkEndOfDocument()) { // unlock if Down at the end of document setScrollLock(false); @@ -311,543 +311,543 @@ public class TextConsoleViewer extends SourceViewer implements LineStyleListener } }); - ColorRegistry colorRegistry = JFaceResources.getColorRegistry(); - propertyChangeListener = new HyperlinkColorChangeListener(); - colorRegistry.addListener(propertyChangeListener); - - revealJob.setSystem(true); - document.addDocumentListener(documentListener); - document.addPositionUpdater(positionUpdater); - } - - /** - * Sets the tab width used by this viewer. - * - * @param tabWidth - * the tab width used by this viewer - */ - public void setTabWidth(int tabWidth) { - StyledText styledText = getTextWidget(); - int oldWidth = styledText.getTabs(); - if (tabWidth != oldWidth) { - styledText.setTabs(tabWidth); - } - } - - /** - * Sets the font used by this viewer. - * - * @param font - * the font used by this viewer - */ - public void setFont(Font font) { - StyledText styledText = getTextWidget(); - Font oldFont = styledText.getFont(); - if (oldFont == font) { - return; - } - if (font == null || !(font.equals(oldFont))) { - styledText.setFont(font); - } - } - - /** - * Positions the cursor at the end of the document. - */ - protected void revealEndOfDocument() { - revealJob.schedule(50); - } - - /* - * (non-Javadoc) - * - * @see org.eclipse.swt.custom.LineStyleListener#lineGetStyle(org.eclipse.swt.custom.LineStyleEvent) - */ - @Override + ColorRegistry colorRegistry = JFaceResources.getColorRegistry(); + propertyChangeListener = new HyperlinkColorChangeListener(); + colorRegistry.addListener(propertyChangeListener); + + revealJob.setSystem(true); + document.addDocumentListener(documentListener); + document.addPositionUpdater(positionUpdater); + } + + /** + * Sets the tab width used by this viewer. + * + * @param tabWidth + * the tab width used by this viewer + */ + public void setTabWidth(int tabWidth) { + StyledText styledText = getTextWidget(); + int oldWidth = styledText.getTabs(); + if (tabWidth != oldWidth) { + styledText.setTabs(tabWidth); + } + } + + /** + * Sets the font used by this viewer. + * + * @param font + * the font used by this viewer + */ + public void setFont(Font font) { + StyledText styledText = getTextWidget(); + Font oldFont = styledText.getFont(); + if (oldFont == font) { + return; + } + if (font == null || !(font.equals(oldFont))) { + styledText.setFont(font); + } + } + + /** + * Positions the cursor at the end of the document. + */ + protected void revealEndOfDocument() { + revealJob.schedule(50); + } + + /* + * (non-Javadoc) + * + * @see org.eclipse.swt.custom.LineStyleListener#lineGetStyle(org.eclipse.swt.custom.LineStyleEvent) + */ + @Override public void lineGetStyle(LineStyleEvent event) { - IDocument document = getDocument(); - if (document != null && document.getLength() > 0) { + IDocument document = getDocument(); + if (document != null && document.getLength() > 0) { ArrayList<StyleRange> ranges = new ArrayList<StyleRange>(); - int offset = event.lineOffset; - int length = event.lineText.length(); - - StyleRange[] partitionerStyles = ((IConsoleDocumentPartitioner) document.getDocumentPartitioner()).getStyleRanges(event.lineOffset, event.lineText.length()); - if (partitionerStyles != null) { - for (int i = 0; i < partitionerStyles.length; i++) { - ranges.add(partitionerStyles[i]); - } - } else { - ranges.add(new StyleRange(offset, length, null, null)); - } - - try { - Position[] positions = getDocument().getPositions(ConsoleHyperlinkPosition.HYPER_LINK_CATEGORY); - Position[] overlap = findPosition(offset, length, positions); - Color color = JFaceColors.getHyperlinkText(Display.getCurrent()); - if (overlap != null) { - for (int i = 0; i < overlap.length; i++) { - Position position = overlap[i]; - StyleRange linkRange = new StyleRange(position.offset, position.length, color, null); - linkRange.underline = true; - override(ranges, linkRange); - } - } - } catch (BadPositionCategoryException e) { - } - - if (ranges.size() > 0) { - event.styles = ranges.toArray(new StyleRange[ranges.size()]); - } - } - } + int offset = event.lineOffset; + int length = event.lineText.length(); + + StyleRange[] partitionerStyles = ((IConsoleDocumentPartitioner) document.getDocumentPartitioner()).getStyleRanges(event.lineOffset, event.lineText.length()); + if (partitionerStyles != null) { + for (int i = 0; i < partitionerStyles.length; i++) { + ranges.add(partitionerStyles[i]); + } + } else { + ranges.add(new StyleRange(offset, length, null, null)); + } + + try { + Position[] positions = getDocument().getPositions(ConsoleHyperlinkPosition.HYPER_LINK_CATEGORY); + Position[] overlap = findPosition(offset, length, positions); + Color color = JFaceColors.getHyperlinkText(Display.getCurrent()); + if (overlap != null) { + for (int i = 0; i < overlap.length; i++) { + Position position = overlap[i]; + StyleRange linkRange = new StyleRange(position.offset, position.length, color, null); + linkRange.underline = true; + override(ranges, linkRange); + } + } + } catch (BadPositionCategoryException e) { + } + + if (ranges.size() > 0) { + event.styles = ranges.toArray(new StyleRange[ranges.size()]); + } + } + } private void override(List<StyleRange> ranges, StyleRange newRange) { - if (ranges.isEmpty()) { - ranges.add(newRange); - return; - } - - int start = newRange.start; - int end = start + newRange.length; - for (int i = 0; i < ranges.size(); i++) { - StyleRange existingRange = ranges.get(i); - int rEnd = existingRange.start + existingRange.length; - if (end <= existingRange.start || start >= rEnd) { - continue; - } - - if (start < existingRange.start && end > existingRange.start) { - start = existingRange.start; - } - - if (start >= existingRange.start && end <= rEnd) { - existingRange.length = start - existingRange.start; - ranges.add(++i, newRange); - if (end != rEnd) { - ranges.add(++i, new StyleRange(end, rEnd - end - 1, existingRange.foreground, existingRange.background)); - } - return; - } else if (start >= existingRange.start && start < rEnd) { - existingRange.length = start - existingRange.start; - ranges.add(++i, newRange); - } else if (end >= rEnd) { - ranges.remove(i); - } else { - ranges.add(++i, new StyleRange(end + 1, rEnd - end + 1, existingRange.foreground, existingRange.background)); - } - } - } - - /** - * Binary search for the positions overlapping the given range - * - * @param offset - * the offset of the range - * @param length - * the length of the range - * @param positions - * the positions to search - * @return the positions overlapping the given range, or <code>null</code> - */ - private Position[] findPosition(int offset, int length, Position[] positions) { - - if (positions.length == 0) { + if (ranges.isEmpty()) { + ranges.add(newRange); + return; + } + + int start = newRange.start; + int end = start + newRange.length; + for (int i = 0; i < ranges.size(); i++) { + StyleRange existingRange = ranges.get(i); + int rEnd = existingRange.start + existingRange.length; + if (end <= existingRange.start || start >= rEnd) { + continue; + } + + if (start < existingRange.start && end > existingRange.start) { + start = existingRange.start; + } + + if (start >= existingRange.start && end <= rEnd) { + existingRange.length = start - existingRange.start; + ranges.add(++i, newRange); + if (end != rEnd) { + ranges.add(++i, new StyleRange(end, rEnd - end - 1, existingRange.foreground, existingRange.background)); + } + return; + } else if (start >= existingRange.start && start < rEnd) { + existingRange.length = start - existingRange.start; + ranges.add(++i, newRange); + } else if (end >= rEnd) { + ranges.remove(i); + } else { + ranges.add(++i, new StyleRange(end + 1, rEnd - end + 1, existingRange.foreground, existingRange.background)); + } + } + } + + /** + * Binary search for the positions overlapping the given range + * + * @param offset + * the offset of the range + * @param length + * the length of the range + * @param positions + * the positions to search + * @return the positions overlapping the given range, or <code>null</code> + */ + private Position[] findPosition(int offset, int length, Position[] positions) { + + if (positions.length == 0) { return null; } - int rangeEnd = offset + length; - int left = 0; - int right = positions.length - 1; - int mid = 0; - Position position = null; + int rangeEnd = offset + length; + int left = 0; + int right = positions.length - 1; + int mid = 0; + Position position = null; - while (left < right) { + while (left < right) { - mid = (left + right) / 2; + mid = (left + right) / 2; - position = positions[mid]; - if (rangeEnd < position.getOffset()) { - if (left == mid) { + position = positions[mid]; + if (rangeEnd < position.getOffset()) { + if (left == mid) { right = left; } else { right = mid - 1; } - } else if (offset > (position.getOffset() + position.getLength() - 1)) { - if (right == mid) { + } else if (offset > (position.getOffset() + position.getLength() - 1)) { + if (right == mid) { left = right; } else { left = mid + 1; } - } else { - left = right = mid; - } - } + } else { + left = right = mid; + } + } List<Position> list = new ArrayList<Position>(); - int index = left - 1; - if (index >= 0) { - position = positions[index]; - while (index >= 0 && (position.getOffset() + position.getLength()) > offset) { - index--; - if (index > 0) { - position = positions[index]; - } - } - } - index++; - position = positions[index]; - while (index < positions.length && (position.getOffset() < rangeEnd)) { - list.add(position); - index++; - if (index < positions.length) { - position = positions[index]; - } - } - - if (list.isEmpty()) { - return null; - } - return list.toArray(new Position[list.size()]); - } - - /* - * (non-Javadoc) - * - * @see org.eclipse.swt.custom.LineBackgroundListener#lineGetBackground(org.eclipse.swt.custom.LineBackgroundEvent) - */ - @Override + int index = left - 1; + if (index >= 0) { + position = positions[index]; + while (index >= 0 && (position.getOffset() + position.getLength()) > offset) { + index--; + if (index > 0) { + position = positions[index]; + } + } + } + index++; + position = positions[index]; + while (index < positions.length && (position.getOffset() < rangeEnd)) { + list.add(position); + index++; + if (index < positions.length) { + position = positions[index]; + } + } + + if (list.isEmpty()) { + return null; + } + return list.toArray(new Position[list.size()]); + } + + /* + * (non-Javadoc) + * + * @see org.eclipse.swt.custom.LineBackgroundListener#lineGetBackground(org.eclipse.swt.custom.LineBackgroundEvent) + */ + @Override public void lineGetBackground(LineBackgroundEvent event) { - event.lineBackground = null; - } - - /** - * Returns the hand cursor. - * - * @return the hand cursor - */ - protected Cursor getHandCursor() { - if (handCursor == null) { - handCursor = new Cursor(ConsolePlugin.getStandardDisplay(), SWT.CURSOR_HAND); - } - return handCursor; - } - - /** - * Returns the text cursor. - * - * @return the text cursor - */ - protected Cursor getTextCursor() { - if (textCursor == null) { - textCursor = new Cursor(ConsolePlugin.getStandardDisplay(), SWT.CURSOR_IBEAM); - } - return textCursor; - } - - /** - * Notification a hyperlink has been entered. - * - * @param link - * the link that was entered - */ - protected void linkEntered(IHyperlink link) { - Control control = getTextWidget(); - if (hyperlink != null) { - linkExited(hyperlink); - } - hyperlink = link; - hyperlink.linkEntered(); - control.setCursor(getHandCursor()); - control.redraw(); - control.addMouseListener(this); - } - - /** - * Notification a link was exited. - * - * @param link - * the link that was exited - */ - protected void linkExited(IHyperlink link) { - link.linkExited(); - hyperlink = null; - Control control = getTextWidget(); - control.setCursor(getTextCursor()); - control.redraw(); - control.removeMouseListener(this); - } - - /* - * (non-Javadoc) - * - * @see org.eclipse.swt.events.MouseTrackListener#mouseEnter(org.eclipse.swt.events.MouseEvent) - */ - @Override + event.lineBackground = null; + } + + /** + * Returns the hand cursor. + * + * @return the hand cursor + */ + protected Cursor getHandCursor() { + if (handCursor == null) { + handCursor = new Cursor(ConsolePlugin.getStandardDisplay(), SWT.CURSOR_HAND); + } + return handCursor; + } + + /** + * Returns the text cursor. + * + * @return the text cursor + */ + protected Cursor getTextCursor() { + if (textCursor == null) { + textCursor = new Cursor(ConsolePlugin.getStandardDisplay(), SWT.CURSOR_IBEAM); + } + return textCursor; + } + + /** + * Notification a hyperlink has been entered. + * + * @param link + * the link that was entered + */ + protected void linkEntered(IHyperlink link) { + Control control = getTextWidget(); + if (hyperlink != null) { + linkExited(hyperlink); + } + hyperlink = link; + hyperlink.linkEntered(); + control.setCursor(getHandCursor()); + control.redraw(); + control.addMouseListener(this); + } + + /** + * Notification a link was exited. + * + * @param link + * the link that was exited + */ + protected void linkExited(IHyperlink link) { + link.linkExited(); + hyperlink = null; + Control control = getTextWidget(); + control.setCursor(getTextCursor()); + control.redraw(); + control.removeMouseListener(this); + } + + /* + * (non-Javadoc) + * + * @see org.eclipse.swt.events.MouseTrackListener#mouseEnter(org.eclipse.swt.events.MouseEvent) + */ + @Override public void mouseEnter(MouseEvent e) { - getTextWidget().addMouseMoveListener(this); - } - - /* - * (non-Javadoc) - * - * @see org.eclipse.swt.events.MouseTrackListener#mouseExit(org.eclipse.swt.events.MouseEvent) - */ - @Override + getTextWidget().addMouseMoveListener(this); + } + + /* + * (non-Javadoc) + * + * @see org.eclipse.swt.events.MouseTrackListener#mouseExit(org.eclipse.swt.events.MouseEvent) + */ + @Override public void mouseExit(MouseEvent e) { - getTextWidget().removeMouseMoveListener(this); - if (hyperlink != null) { - linkExited(hyperlink); - } - } - - /* - * (non-Javadoc) - * - * @see org.eclipse.swt.events.MouseTrackListener#mouseHover(org.eclipse.swt.events.MouseEvent) - */ - @Override + getTextWidget().removeMouseMoveListener(this); + if (hyperlink != null) { + linkExited(hyperlink); + } + } + + /* + * (non-Javadoc) + * + * @see org.eclipse.swt.events.MouseTrackListener#mouseHover(org.eclipse.swt.events.MouseEvent) + */ + @Override public void mouseHover(MouseEvent e) { - } - - /* - * (non-Javadoc) - * - * @see org.eclipse.swt.events.MouseMoveListener#mouseMove(org.eclipse.swt.events.MouseEvent) - */ - @Override + } + + /* + * (non-Javadoc) + * + * @see org.eclipse.swt.events.MouseMoveListener#mouseMove(org.eclipse.swt.events.MouseEvent) + */ + @Override public void mouseMove(MouseEvent e) { - int offset = -1; - try { - Point p = new Point(e.x, e.y); - offset = getTextWidget().getOffsetAtLocation(p); - } catch (IllegalArgumentException ex) { - // out of the document range - } - updateLinks(offset); - } - - /** - * The cursor has just be moved to the given offset, the mouse has hovered - * over the given offset. Update link rendering. - * - * @param offset - */ - protected void updateLinks(int offset) { - if (offset >= 0) { - IHyperlink link = getHyperlink(offset); - if (link != null) { - if (link.equals(hyperlink)) { - return; - } - linkEntered(link); - return; - } - } - if (hyperlink != null) { - linkExited(hyperlink); - } - } - - /** - * Returns the currently active hyperlink or <code>null</code> if none. - * - * @return the currently active hyperlink or <code>null</code> if none - */ - public IHyperlink getHyperlink() { - return hyperlink; - } - - /** - * Returns the hyperlink at the specified offset, or <code>null</code> if - * none. - * - * @param offset - * offset at which a hyperlink has been requested - * @return hyperlink at the specified offset, or <code>null</code> if none - */ - public IHyperlink getHyperlink(int offset) { - if (offset >= 0 && console != null) { - return console.getHyperlink(offset); - } - return null; - } - - /* - * (non-Javadoc) - * - * @see org.eclipse.swt.events.MouseListener#mouseDoubleClick(org.eclipse.swt.events.MouseEvent) - */ - @Override + int offset = -1; + try { + Point p = new Point(e.x, e.y); + offset = getTextWidget().getOffsetAtLocation(p); + } catch (IllegalArgumentException ex) { + // out of the document range + } + updateLinks(offset); + } + + /** + * The cursor has just be moved to the given offset, the mouse has hovered + * over the given offset. Update link rendering. + * + * @param offset + */ + protected void updateLinks(int offset) { + if (offset >= 0) { + IHyperlink link = getHyperlink(offset); + if (link != null) { + if (link.equals(hyperlink)) { + return; + } + linkEntered(link); + return; + } + } + if (hyperlink != null) { + linkExited(hyperlink); + } + } + + /** + * Returns the currently active hyperlink or <code>null</code> if none. + * + * @return the currently active hyperlink or <code>null</code> if none + */ + public IHyperlink getHyperlink() { + return hyperlink; + } + + /** + * Returns the hyperlink at the specified offset, or <code>null</code> if + * none. + * + * @param offset + * offset at which a hyperlink has been requested + * @return hyperlink at the specified offset, or <code>null</code> if none + */ + public IHyperlink getHyperlink(int offset) { + if (offset >= 0 && console != null) { + return console.getHyperlink(offset); + } + return null; + } + + /* + * (non-Javadoc) + * + * @see org.eclipse.swt.events.MouseListener#mouseDoubleClick(org.eclipse.swt.events.MouseEvent) + */ + @Override public void mouseDoubleClick(MouseEvent e) { - } - - /* - * (non-Javadoc) - * - * @see org.eclipse.swt.events.MouseListener#mouseDown(org.eclipse.swt.events.MouseEvent) - */ - @Override + } + + /* + * (non-Javadoc) + * + * @see org.eclipse.swt.events.MouseListener#mouseDown(org.eclipse.swt.events.MouseEvent) + */ + @Override public void mouseDown(MouseEvent e) { - } - - /* - * (non-Javadoc) - * - * @see org.eclipse.swt.events.MouseListener#mouseUp(org.eclipse.swt.events.MouseEvent) - */ - @Override + } + + /* + * (non-Javadoc) + * + * @see org.eclipse.swt.events.MouseListener#mouseUp(org.eclipse.swt.events.MouseEvent) + */ + @Override public void mouseUp(MouseEvent e) { - } + } - /* - * (non-Javadoc) - * - * @see org.eclipse.jface.text.TextViewer#createDocumentAdapter() - */ + /* + * (non-Javadoc) + * + * @see org.eclipse.jface.text.TextViewer#createDocumentAdapter() + */ @Override protected IDocumentAdapter createDocumentAdapter() { - if (documentAdapter == null) { - documentAdapter = new ConsoleDocumentAdapter(consoleWidth = -1); - } - return documentAdapter; - } - - /** - * Sets the console to have a fixed character width. Use -1 to indicate that - * a fixed width should not be used. - * - * @param width - * fixed character width of the console, or -1 - */ - public void setConsoleWidth(int width) { - if (consoleWidth != width) { - consoleWidth = width; - ConsolePlugin.getStandardDisplay().asyncExec(new Runnable() { - @Override + if (documentAdapter == null) { + documentAdapter = new ConsoleDocumentAdapter(consoleWidth = -1); + } + return documentAdapter; + } + + /** + * Sets the console to have a fixed character width. Use -1 to indicate that + * a fixed width should not be used. + * + * @param width + * fixed character width of the console, or -1 + */ + public void setConsoleWidth(int width) { + if (consoleWidth != width) { + consoleWidth = width; + ConsolePlugin.getStandardDisplay().asyncExec(new Runnable() { + @Override public void run() { - if (documentAdapter != null) { - documentAdapter.setWidth(consoleWidth); - } - } - }); - } - } - - /* - * (non-Javadoc) - * - * @see org.eclipse.jface.text.TextViewer#handleDispose() - */ - @Override + if (documentAdapter != null) { + documentAdapter.setWidth(consoleWidth); + } + } + }); + } + } + + /* + * (non-Javadoc) + * + * @see org.eclipse.jface.text.TextViewer#handleDispose() + */ + @Override protected void handleDispose() { - IDocument document = getDocument(); - if (document != null) { - document.removeDocumentListener(documentListener); - document.removePositionUpdater(positionUpdater); - } - - StyledText styledText = getTextWidget(); - styledText.removeLineStyleListener(this); - styledText.removeLineBackgroundListener(this); - styledText.removeMouseTrackListener(this); - - if(handCursor != null) { - handCursor.dispose(); - } - handCursor = null; - if(textCursor != null) { - textCursor.dispose(); - } - textCursor = null; - hyperlink = null; - console = null; - - ColorRegistry colorRegistry = JFaceResources.getColorRegistry(); - colorRegistry.removeListener(propertyChangeListener); - - super.handleDispose(); - } - - class HyperlinkColorChangeListener implements IPropertyChangeListener { - @Override + IDocument document = getDocument(); + if (document != null) { + document.removeDocumentListener(documentListener); + document.removePositionUpdater(positionUpdater); + } + + StyledText styledText = getTextWidget(); + styledText.removeLineStyleListener(this); + styledText.removeLineBackgroundListener(this); + styledText.removeMouseTrackListener(this); + + if(handCursor != null) { + handCursor.dispose(); + } + handCursor = null; + if(textCursor != null) { + textCursor.dispose(); + } + textCursor = null; + hyperlink = null; + console = null; + + ColorRegistry colorRegistry = JFaceResources.getColorRegistry(); + colorRegistry.removeListener(propertyChangeListener); + + super.handleDispose(); + } + + class HyperlinkColorChangeListener implements IPropertyChangeListener { + @Override public void propertyChange(PropertyChangeEvent event) { - if (event.getProperty().equals(JFacePreferences.ACTIVE_HYPERLINK_COLOR) || event.getProperty().equals(JFacePreferences.HYPERLINK_COLOR)) { - getTextWidget().redraw(); - } - } + if (event.getProperty().equals(JFacePreferences.ACTIVE_HYPERLINK_COLOR) || event.getProperty().equals(JFacePreferences.HYPERLINK_COLOR)) { + getTextWidget().redraw(); + } + } - } + } - /* - * work around to memory leak in TextViewer$WidgetCommand - */ - @Override + /* + * work around to memory leak in TextViewer$WidgetCommand + */ + @Override protected void updateTextListeners(WidgetCommand cmd) { - super.updateTextListeners(cmd); - cmd.preservedText = null; - cmd.event = null; - cmd.text = null; - } + super.updateTextListeners(cmd); + cmd.preservedText = null; + cmd.event = null; + cmd.text = null; + } - @Override + @Override protected void internalRevealRange(int start, int end) { - StyledText textWidget = getTextWidget(); - int startLine = documentAdapter.getLineAtOffset(start); - int endLine = documentAdapter.getLineAtOffset(end); + StyledText textWidget = getTextWidget(); + int startLine = documentAdapter.getLineAtOffset(start); + int endLine = documentAdapter.getLineAtOffset(end); - int top = textWidget.getTopIndex(); - if (top > -1) { - // scroll vertically + int top = textWidget.getTopIndex(); + if (top > -1) { + // scroll vertically @SuppressWarnings("deprecation") int lines = getVisibleLinesInViewport(); - int bottom = top + lines; - - // two lines at the top and the bottom should always be left - // if window is smaller than 5 lines, always center position is - // chosen - int bufferZone = 2; - if (startLine >= top + bufferZone && startLine <= bottom - bufferZone && endLine >= top + bufferZone && endLine <= bottom - bufferZone) { - - // do not scroll at all as it is already visible - } else { - int delta = Math.max(0, lines - (endLine - startLine)); - textWidget.setTopIndex(startLine - delta / 3); - updateViewportListeners(INTERNAL); - } - - // scroll horizontally - if (endLine < startLine) { - endLine += startLine; - startLine = endLine - startLine; - endLine -= startLine; - } - - int startPixel = -1; - int endPixel = -1; - - if (endLine > startLine) { - // reveal the beginning of the range in the start line - IRegion extent = getExtent(start, start); - startPixel = extent.getOffset() + textWidget.getHorizontalPixel(); - endPixel = startPixel; - } else { - IRegion extent = getExtent(start, end); - startPixel = extent.getOffset() + textWidget.getHorizontalPixel(); - endPixel = startPixel + extent.getLength(); - } - - int visibleStart = textWidget.getHorizontalPixel(); - int visibleEnd = visibleStart + textWidget.getClientArea().width; - - // scroll only if not yet visible - if (startPixel < visibleStart || visibleEnd < endPixel) { - // set buffer zone to 10 pixels - bufferZone = 10; - int newOffset = visibleStart; - int visibleWidth = visibleEnd - visibleStart; - int selectionPixelWidth = endPixel - startPixel; - - if (startPixel < visibleStart) { + int bottom = top + lines; + + // two lines at the top and the bottom should always be left + // if window is smaller than 5 lines, always center position is + // chosen + int bufferZone = 2; + if (startLine >= top + bufferZone && startLine <= bottom - bufferZone && endLine >= top + bufferZone && endLine <= bottom - bufferZone) { + + // do not scroll at all as it is already visible + } else { + int delta = Math.max(0, lines - (endLine - startLine)); + textWidget.setTopIndex(startLine - delta / 3); + updateViewportListeners(INTERNAL); + } + + // scroll horizontally + if (endLine < startLine) { + endLine += startLine; + startLine = endLine - startLine; + endLine -= startLine; + } + + int startPixel = -1; + int endPixel = -1; + + if (endLine > startLine) { + // reveal the beginning of the range in the start line + IRegion extent = getExtent(start, start); + startPixel = extent.getOffset() + textWidget.getHorizontalPixel(); + endPixel = startPixel; + } else { + IRegion extent = getExtent(start, end); + startPixel = extent.getOffset() + textWidget.getHorizontalPixel(); + endPixel = startPixel + extent.getLength(); + } + + int visibleStart = textWidget.getHorizontalPixel(); + int visibleEnd = visibleStart + textWidget.getClientArea().width; + + // scroll only if not yet visible + if (startPixel < visibleStart || visibleEnd < endPixel) { + // set buffer zone to 10 pixels + bufferZone = 10; + int newOffset = visibleStart; + int visibleWidth = visibleEnd - visibleStart; + int selectionPixelWidth = endPixel - startPixel; + + if (startPixel < visibleStart) { newOffset = startPixel; } else if (selectionPixelWidth + bufferZone < visibleWidth) { newOffset = endPixel + bufferZone - visibleWidth; @@ -855,13 +855,13 @@ public class TextConsoleViewer extends SourceViewer implements LineStyleListener newOffset = startPixel; } - float index = ((float) newOffset) / ((float) getAverageCharWidth()); + float index = ((float) newOffset) / ((float) getAverageCharWidth()); - textWidget.setHorizontalIndex(Math.round(index)); - } + textWidget.setHorizontalIndex(Math.round(index)); + } - } - } + } + } } |