001: /*
002: * FindBugs - Find Bugs in Java programs
003: * Copyright (C) 2006, University of Maryland
004: *
005: * This library is free software; you can redistribute it and/or
006: * modify it under the terms of the GNU Lesser General Public
007: * License as published by the Free Software Foundation; either
008: * version 2.1 of the License, or (at your option) any later version.
009: *
010: * This library is distributed in the hope that it will be useful,
011: * but WITHOUT ANY WARRANTY; without even the implied warranty of
012: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
013: * Lesser General Public License for more details.
014: *
015: * You should have received a copy of the GNU Lesser General Public
016: * License along with this library; if not, write to the Free Software
017: * Foundation, Inc., 59 Temple Place, Suite 330, Boston MA 02111-1307, USA
018: */
019:
020: package edu.umd.cs.findbugs.sourceViewer;
021:
022: import java.awt.Container;
023: import java.awt.Rectangle;
024: import java.io.Serializable;
025: import java.util.Collection;
026: import java.util.Comparator;
027: import java.util.PriorityQueue;
028:
029: import javax.swing.JTextPane;
030: import javax.swing.SwingUtilities;
031: import javax.swing.text.BadLocationException;
032: import javax.swing.text.Document;
033: import javax.swing.text.Element;
034: import javax.swing.text.StyledDocument;
035:
036: import edu.umd.cs.findbugs.gui2.MainFrame;
037:
038: /**
039: * @author tuc
040: */
041: public class NavigableTextPane extends JTextPane {
042:
043: public NavigableTextPane() {
044: }
045:
046: public NavigableTextPane(StyledDocument doc) {
047: super (doc);
048: }
049:
050: /** return the height of the parent (which is presumably a JViewport).
051: * If there is no parent, return this.getHeight(). */
052: private int parentHeight() {
053: Container parent = getParent();
054: if (parent != null)
055: return parent.getHeight();
056: return getHeight(); // entire pane height, may be huge
057: }
058:
059: public int getLineOffset(int line) throws BadLocationException {
060: return lineToOffset(line);
061: }
062:
063: private int lineToOffset(int line) throws BadLocationException {
064: Document d = getDocument();
065: try {
066: Element element = d.getDefaultRootElement().getElement(
067: line - 1);
068: if (element == null)
069: throw new BadLocationException("line " + line
070: + " does not exist", -line);
071: return element.getStartOffset();
072: } catch (ArrayIndexOutOfBoundsException aioobe) {
073: BadLocationException ble = new BadLocationException("line "
074: + line + " does not exist", -line);
075: ble.initCause(aioobe);
076: throw ble;
077: }
078: }
079:
080: private int offsetToY(int offset) throws BadLocationException {
081: Rectangle r = modelToView(offset);
082: return r.y;
083: }
084:
085: private int lineToY(int line) throws BadLocationException {
086: return offsetToY(lineToOffset(line));
087: }
088:
089: private void scrollYToVisibleImpl(int y, int margin) {
090: final Rectangle r = new Rectangle(0, y - margin, 4, 2 * margin);
091:
092: SwingUtilities.invokeLater(new Runnable() {
093: public void run() {
094: scrollRectToVisible(r);
095: }
096: });
097: }
098:
099: private void scrollLineToVisibleImpl(int line, int margin) {
100: try {
101: int y = lineToY(line);
102: scrollYToVisibleImpl(y, margin);
103: } catch (BadLocationException ble) {
104: if (MainFrame.DEBUG)
105: ble.printStackTrace();
106: }
107: }
108:
109: /** scroll the specified line into view, with a margin of 'margin' pixels above and below */
110: public void scrollLineToVisible(int line, int margin) {
111: int maxMargin = (parentHeight() - 20) / 2;
112: if (margin > maxMargin)
113: margin = Math.max(0, maxMargin);
114: scrollLineToVisibleImpl(line, margin);
115: }
116:
117: /** scroll the specified line into the middle third of the view */
118: public void scrollLineToVisible(int line) {
119: int margin = parentHeight() / 3;
120: scrollLineToVisibleImpl(line, margin);
121: }
122:
123: /** scroll the specified primary lines into view, along
124: * with as many of the other lines as is convenient */
125: public void scrollLinesToVisible(int startLine, int endLine,
126: Collection<Integer> otherLines) {
127: int startY, endY;
128: try {
129: startY = lineToY(startLine);
130: } catch (BadLocationException ble) {
131: if (MainFrame.DEBUG)
132: ble.printStackTrace();
133: return; // give up
134: }
135: try {
136: endY = lineToY(endLine);
137: } catch (BadLocationException ble) {
138: endY = startY; // better than nothing
139: }
140:
141: int max = parentHeight() - 0;
142: if (endY - startY > max) {
143: endY = startY + max;
144: } else if (otherLines != null && otherLines.size() > 0) {
145: int origin = startY + endY / 2;
146: PriorityQueue<Integer> pq = new PriorityQueue<Integer>(
147: otherLines.size(), new DistanceComparator(origin));
148: for (int line : otherLines) {
149: int otherY;
150: try {
151: otherY = lineToY(line);
152: } catch (BadLocationException ble) {
153: continue; // give up on this one
154: }
155: pq.add(otherY);
156: }
157:
158: while (!pq.isEmpty()) {
159: int y = pq.remove();
160: int lo = Math.min(startY, y);
161: int hi = Math.max(endY, y);
162: if (hi - lo > max)
163: break;
164: else {
165: startY = lo;
166: endY = hi;
167: }
168: }
169: }
170: scrollYToVisibleImpl((startY + endY) / 2, max / 2);
171: }
172:
173: public static class DistanceComparator implements
174: Comparator<Integer>, Serializable {
175: private final int origin;
176:
177: public DistanceComparator(int origin) {
178: this .origin = origin;
179: }
180:
181: /* Returns a negative integer, zero, or a positive integer as
182: * the first argument is farther from, equadistant, or closer
183: * to (respectively) the origin.
184: * This sounds backwards, but this way closer values get a
185: * higher priority in the priority queue. */
186: public int compare(Integer a, Integer b) {
187: return Math.abs(b - origin) - Math.abs(a - origin);
188: }
189: }
190:
191: }
|