File Source: TextPane.java
/*
P/P * Method: com.dmdirc.addons.ui_swing.textpane.TextPane__static_init
*/
1 /*
2 * Copyright (c) 2006-2009 Chris Smith, Shane Mc Cormack, Gregory Holmes
3 *
4 * Permission is hereby granted, free of charge, to any person obtaining a copy
5 * of this software and associated documentation files (the "Software"), to deal
6 * in the Software without restriction, including without limitation the rights
7 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
8 * copies of the Software, and to permit persons to whom the Software is
9 * furnished to do so, subject to the following conditions:
10 *
11 * The above copyright notice and this permission notice shall be included in
12 * all copies or substantial portions of the Software.
13 *
14 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
19 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
20 * SOFTWARE.
21 */
22
23 package com.dmdirc.addons.ui_swing.textpane;
24
25 import com.dmdirc.FrameContainer;
26
27 import java.awt.Point;
28 import java.awt.Toolkit;
29 import java.awt.datatransfer.StringSelection;
30 import java.awt.event.AdjustmentEvent;
31 import java.awt.event.AdjustmentListener;
32 import java.awt.event.MouseEvent;
33 import java.awt.event.MouseMotionAdapter;
34 import java.awt.event.MouseMotionListener;
35 import java.awt.event.MouseWheelEvent;
36 import java.awt.event.MouseWheelListener;
37
38 import javax.swing.JComponent;
39 import javax.swing.JScrollBar;
40
41 import net.miginfocom.swing.MigLayout;
42
43 /**
44 * Styled, scrollable text pane.
45 */
/*
P/P * Method: TextPaneCanvas access$100(TextPane)
*
* Preconditions:
* x0 != null
*
* Postconditions:
* return_value == x0.canvas
* init'ed(return_value)
*/
46 public final class TextPane extends JComponent implements AdjustmentListener,
47 MouseWheelListener, IRCDocumentListener {
48
49 /**
50 * A version number for this class. It should be changed whenever the class
51 * structure is changed (or anything else that would prevent serialized
52 * objects being unserialized with the new class).
53 */
54 private static final long serialVersionUID = 5;
55 /** Scrollbar for the component. */
56 private final JScrollBar scrollBar;
57 /** Canvas object, used to draw text. */
58 private final TextPaneCanvas canvas;
59 /** IRCDocument. */
60 private final IRCDocument document;
61 /** Parent Frame. */
62 private final FrameContainer frame;
63
64 /**
65 * Creates a new instance of TextPane.
66 *
67 * @param frame Parent Frame
68 */
69 public TextPane(final FrameContainer frame) {
/*
P/P * Method: void com.dmdirc.addons.ui_swing.textpane.TextPane(FrameContainer)
*
* Preconditions:
* frame != null
*
* Presumptions:
* com.dmdirc.FrameContainer:getConfigManager(...).listeners@75 != null
* com.dmdirc.FrameContainer:getConfigManager(...)@75 != null
*
* Postconditions:
* this.canvas == &new TextPaneCanvas(TextPane#4)
* this.document == &new IRCDocument(TextPane#2)
* this.canvas.document == &new IRCDocument(TextPane#2)
* this.frame == frame
* this.frame != null
* this.scrollBar == &new JScrollBar(TextPane#5)
* new ArrayList(IRCDocument#1) num objects == 1
* new EventListenerList(IRCDocument#2) num objects == 1
* new HashMap(TextPaneCanvas#1) num objects == 1
* new HashMap(TextPaneCanvas#2) num objects == 1
* ...
*/
70 super();
71 setUI(new TextPaneUI());
72
73 this.frame = frame;
74 document = new IRCDocument(frame.getConfigManager());
75 frame.getConfigManager().addChangeListener("ui", "textPaneFontName", document);
76 //TODO issue 2251
77 //frame.getConfigManager().addChangeListener("ui", "textPaneFontSize", document);
78
79 setLayout(new MigLayout("fill"));
80 canvas = new TextPaneCanvas(this, document);
81 add(canvas, "dock center");
82 scrollBar = new JScrollBar(JScrollBar.VERTICAL);
83 add(scrollBar, "dock east");
84 scrollBar.setMaximum(document.getNumLines());
85 scrollBar.setBlockIncrement(10);
86 scrollBar.setUnitIncrement(1);
87 scrollBar.addAdjustmentListener(this);
88
89 addMouseWheelListener(this);
90 document.addIRCDocumentListener(this);
91 setAutoscrolls(true);
92
/*
P/P * Method: void com.dmdirc.addons.ui_swing.textpane.TextPane$1(TextPane)
*/
93 MouseMotionListener doScrollRectToVisible = new MouseMotionAdapter() {
94
95 /** {@inheritDoc} */
96 @Override
97 public void mouseDragged(MouseEvent e) {
/*
P/P * Method: void mouseDragged(MouseEvent)
*
* Preconditions:
* e != null
* (soft) init'ed(this.canvas.scrollBarPosition)
* (soft) this.canvas != null
* (soft) this.canvas.positions != null
* (soft) this.canvas.selection != null
* (soft) this.canvas.textLayouts != null
* (soft) this.canvas.textPane != null
* (soft) this.scrollBar != null
*
* Presumptions:
* com.dmdirc.addons.ui_swing.textpane.TextPane:getLocationOnScreen(...)@102 != null
* com.dmdirc.addons.ui_swing.textpane.TextPane:getLocationOnScreen(...)@104 != null
* com.dmdirc.addons.ui_swing.textpane.TextPane:getLocationOnScreen(...)@98 != null
* javax.swing.JScrollBar:getValue(...)@103 >= -231+1
* javax.swing.JScrollBar:getValue(...)@106 <= 232-2
*
* Postconditions:
* init'ed(this.canvas.scrollBarPosition)
*
* Test Vectors:
* java.awt.event.MouseEvent:getModifiersEx(...)@98: {-231..1_023, 1_025..232-1}, {1_024}
*/
98 if (e.getXOnScreen() > getLocationOnScreen().getX() && e.
99 getXOnScreen() < (getLocationOnScreen().
100 getX() + getWidth()) && e.getModifiersEx() ==
101 MouseEvent.BUTTON1_DOWN_MASK) {
102 if (getLocationOnScreen().getY() > e.getYOnScreen()) {
103 setScrollBarPosition(scrollBar.getValue() - 1);
104 } else if (getLocationOnScreen().getY() + getHeight() <
105 e.getYOnScreen()) {
106 setScrollBarPosition(scrollBar.getValue() + 1);
107 }
108 canvas.highlightEvent(MouseEventType.DRAG, e);
109 }
110 }
111 };
112 addMouseMotionListener(doScrollRectToVisible);
113 }
114
115 /** {@inheritDoc} */
116 @Override
117 public void updateUI() {
/*
P/P * Method: void updateUI()
*/
118 setUI(new TextPaneUI());
119 }
120
121 /**
122 * Sets the new position for the scrollbar and the associated position
123 * to render the text from.
124 * @param position new position of the scrollbar
125 */
126 public void setScrollBarPosition(final int position) {
/*
P/P * Method: void setScrollBarPosition(int)
*
* Preconditions:
* init'ed(this.canvas.scrollBarPosition)
* this.canvas != null
* this.scrollBar != null
* (soft) this.canvas.textPane != null
*
* Postconditions:
* this.canvas.scrollBarPosition == One-of{old this.canvas.scrollBarPosition, position}
* init'ed(this.canvas.scrollBarPosition)
*/
127 scrollBar.setValue(position);
128 canvas.setScrollBarPosition(position);
129 }
130
131 /**
132 * Returns the last visible line in the textpane.
133 *
134 * @return Last visible line index
135 */
136 public int getLastVisibleLine() {
/*
P/P * Method: int getLastVisibleLine()
*
* Preconditions:
* this.scrollBar != null
*
* Postconditions:
* init'ed(return_value)
*/
137 return scrollBar.getValue();
138 }
139
140 /**
141 * Sets the scrollbar's maximum position. If the current position is
142 * within <code>linesAllowed</code> of the end of the document, the
143 * scrollbar's current position is set to the end of the document.
144 *
145 * @param linesAllowed The number of lines allowed below the current position
146 * @since 0.6
147 */
148 protected void setScrollBarMax(final int linesAllowed) {
/*
P/P * Method: void setScrollBarMax(int)
*
* Preconditions:
* this.document != null
* this.document.lines != null
* this.scrollBar != null
* (soft) init'ed(this.canvas.scrollBarPosition)
* (soft) this.canvas != null
* (soft) this.canvas.textPane != null
*
* Presumptions:
* getNumLines(...)@149 in range
* getNumLines(...)@149 - linesAllowed in range
* java.util.List:size(...)@78 >= -231+1
* java.util.List:size(...)@78 - linesAllowed in {-231+1..232}
*
* Postconditions:
* init'ed(this.canvas.scrollBarPosition)
*
* Test Vectors:
* java.util.List:size(...)@78: {-231+1..0, 2..232-1}, {1}
* java.util.List:size(...)@78 - linesAllowed: {0}, {-231+1..-1, 1..232}
* javax.swing.JScrollBar:getValueIsAdjusting(...)@164: {1}, {0}
*/
149 final int lines = document.getNumLines() - 1;
150 final int currentLine = scrollBar.getValue();
151 final int allowedDeviation = lines - linesAllowed;
152
153 if (lines == 0) {
154 canvas.repaint();
155 }
156
157 scrollBar.setMaximum(lines);
158
159 boolean setToMax = currentLine == allowedDeviation;
160 if (allowedDeviation == -1) {
161 setToMax = true;
162 }
163
164 if (!scrollBar.getValueIsAdjusting() && setToMax) {
165 setScrollBarPosition(lines);
166 }
167 }
168
169 /**
170 * {@inheritDoc}
171 *
172 * @param e Mouse wheel event
173 */
174 @Override
175 public void adjustmentValueChanged(final AdjustmentEvent e) {
/*
P/P * Method: void adjustmentValueChanged(AdjustmentEvent)
*
* Preconditions:
* e != null
* init'ed(this.canvas.scrollBarPosition)
* this.canvas != null
* this.scrollBar != null
* (soft) this.canvas.textPane != null
*
* Postconditions:
* init'ed(this.canvas.scrollBarPosition)
*/
176 setScrollBarPosition(e.getValue());
177 }
178
179 /**
180 * {@inheritDoc}
181 *
182 * @param e Mouse wheel event
183 */
184 @Override
185 public void mouseWheelMoved(final MouseWheelEvent e) {
/*
P/P * Method: void mouseWheelMoved(MouseWheelEvent)
*
* Preconditions:
* this.scrollBar != null
* (soft) e != null
* (soft) init'ed(this.canvas.scrollBarPosition)
* (soft) this.canvas != null
* (soft) this.canvas.textPane != null
*
* Presumptions:
* java.awt.event.MouseWheelEvent:getScrollAmount(...)@190 - javax.swing.JScrollBar:getValue(...)@190 in {-232+1..231}
* javax.swing.JScrollBar:getValue(...)@188 + java.awt.event.MouseWheelEvent:getScrollAmount(...)@188 in {-231..232-1}
*
* Postconditions:
* init'ed(this.canvas.scrollBarPosition)
*
* Test Vectors:
* java.awt.event.MouseWheelEvent:getWheelRotation(...)@187: {-231..0}, {1..232-1}
* javax.swing.JScrollBar:isEnabled(...)@186: {0}, {1}
*/
186 if (scrollBar.isEnabled()) {
187 if (e.getWheelRotation() > 0) {
188 setScrollBarPosition(scrollBar.getValue() + e.getScrollAmount());
189 } else {
190 setScrollBarPosition(scrollBar.getValue() - e.getScrollAmount());
191 }
192 }
193 }
194
195 /**
196 *
197 * Returns the line information from a mouse click inside the textpane.
198 *
199 * @param point mouse position
200 *
201 * @return line number, line part, position in whole line
202 */
203 public LineInfo getClickPosition(final Point point) {
/*
P/P * Method: LineInfo getClickPosition(Point)
*
* Preconditions:
* this.canvas != null
* (soft) this.canvas.positions != null
* (soft) this.canvas.textLayouts != null
*
* Postconditions:
* return_value == &new LineInfo(getClickPosition#1*)
* new LineInfo(getClickPosition#1*) num objects == 1
* init'ed(new LineInfo(getClickPosition#1*).index)
* init'ed(new LineInfo(getClickPosition#1*).line)
* init'ed(new LineInfo(getClickPosition#1*).part)
*/
204 return canvas.getClickPosition(point);
205 }
206
207 /**
208 * Returns the selected text.
209 *
210 * <li>0 = start line</li>
211 * <li>1 = start char</li>
212 * <li>2 = end line</li>
213 * <li>3 = end char</li>
214 *
215 * @return Selected text
216 */
217 public String getSelectedText() {
/*
P/P * Method: String getSelectedText()
*
* Preconditions:
* this.canvas != null
* this.canvas.selection != null
* init'ed(this.canvas.selection.endLine)
* init'ed(this.canvas.selection.endPos)
* init'ed(this.canvas.selection.startLine)
* init'ed(this.canvas.selection.startPos)
* (soft) this.document != null
* (soft) this.document.lines != null
*
* Presumptions:
* com.dmdirc.ui.messages.Styliser:stipControlCodes(...)@107 != null
* getLine(...).lineParts != null
* getLine(...).lineParts.length <= 232-1
* java.util.List:get(...)@89 != null
*
* Postconditions:
* java.lang.StringBuffer:toString(...)._tainted == 0
* return_value in Addr_Set{null,&java.lang.StringBuffer:toString(...),&java.lang.StringBuffer:toString(...)}
*
* Test Vectors:
* java.lang.String:isEmpty(...)@235: {1}, {0}
*/
218 final StringBuffer selectedText = new StringBuffer();
219 final LinePosition selectedRange = canvas.getSelectedRange();
220
221 if (selectedRange.getStartLine() == -1) {
222 return null;
223 }
224
225 for (int i = selectedRange.getStartLine(); i <=
226 selectedRange.getEndLine();
227 i++) {
228 if (i != selectedRange.getStartLine()) {
229 selectedText.append('\n');
230 }
231 if (document.getNumLines() <= i) {
232 return selectedText.toString();
233 }
234 final String line = document.getLine(i).getText();
235 if (!line.isEmpty()) {
236 if (selectedRange.getEndLine() == selectedRange.getStartLine()) {
237 //loop through range
238 if (selectedRange.getStartPos() != -1
239 && selectedRange.getEndPos() != -1) {
240 selectedText.append(line.substring(
241 selectedRange.getStartPos(),
242 selectedRange.getEndPos()));
243 }
244 } else if (i == selectedRange.getStartLine()) {
245 //loop from start of range to the end
246 if (selectedRange.getStartPos() != -1) {
247 selectedText.append(line.substring(
248 selectedRange.getStartPos(), line.length()));
249 }
250 } else if (i == selectedRange.getEndLine()) {
251 //loop from start to end of range
252 if (selectedRange.getEndPos() != -1) {
253 selectedText.append(line.substring(0, selectedRange.
254 getEndPos()));
255 }
256 } else {
257 //loop the whole line
258 selectedText.append(line);
259 }
260 }
261 }
262
263 return selectedText.toString();
264 }
265
266 /**
267 * Returns the selected range.
268 *
269 * @return selected range
270 */
271 public LinePosition getSelectedRange() {
/*
P/P * Method: LinePosition getSelectedRange()
*
* Preconditions:
* this.canvas != null
* this.canvas.selection != null
* init'ed(this.canvas.selection.endLine)
* init'ed(this.canvas.selection.endPos)
* init'ed(this.canvas.selection.startLine)
* init'ed(this.canvas.selection.startPos)
*
* Postconditions:
* return_value == One-of{&new LinePosition(getSelectedRange#1*), &new LinePosition(getSelectedRange#2*), &new LinePosition(getSelectedRange#3*)}
* return_value in Addr_Set{&new LinePosition(getSelectedRange#1*),&new LinePosition(getSelectedRange#2*),&new LinePosition(getSelectedRange#3*)}
* new LinePosition(getSelectedRange#1*) num objects <= 1
* new LinePosition(getSelectedRange#1*).endLine == this.canvas.selection.startLine
* new LinePosition(getSelectedRange#1*).endLine >= -231+1
* new LinePosition(getSelectedRange#1*).endPos == this.canvas.selection.startPos
* init'ed(new LinePosition(getSelectedRange#1*).endPos)
* new LinePosition(getSelectedRange#1*).startLine == this.canvas.selection.endLine
* new LinePosition(getSelectedRange#1*).startLine <= 232-2
* new LinePosition(getSelectedRange#1*).startPos == this.canvas.selection.endPos
* ...
*/
272 return canvas.getSelectedRange();
273 }
274
275 /**
276 * Returns whether there is a selected range.
277 *
278 * @return true iif there is a selected range
279 */
280 public boolean hasSelectedRange() {
/*
P/P * Method: bool hasSelectedRange()
*
* Preconditions:
* this.canvas != null
* this.canvas.selection != null
* init'ed(this.canvas.selection.endLine)
* init'ed(this.canvas.selection.endPos)
* init'ed(this.canvas.selection.startLine)
* init'ed(this.canvas.selection.startPos)
*
* Postconditions:
* init'ed(return_value)
*/
281 final LinePosition selectedRange = canvas.getSelectedRange();
282 return !(selectedRange.getStartLine() == selectedRange.getEndLine() &&
283 selectedRange.getStartPos() == selectedRange.getEndPos());
284 }
285
286 /**
287 * Selects the specified region of text.
288 *
289 * @param position Line position
290 */
291 public void setSelectedTexT(final LinePosition position) {
/*
P/P * Method: void setSelectedTexT(LinePosition)
*
* Preconditions:
* position != null
* init'ed(position.endLine)
* init'ed(position.endPos)
* init'ed(position.startLine)
* init'ed(position.startPos)
* this.canvas != null
*
* Postconditions:
* this.canvas.selection == &new LinePosition(setSelectedRange#1)
* new LinePosition(setSelectedRange#1) num objects == 1
* new LinePosition(setSelectedRange#1).endLine == position.endLine
* init'ed(new LinePosition(setSelectedRange#1).endLine)
* new LinePosition(setSelectedRange#1).endPos == position.endPos
* init'ed(new LinePosition(setSelectedRange#1).endPos)
* new LinePosition(setSelectedRange#1).startLine == position.startLine
* init'ed(new LinePosition(setSelectedRange#1).startLine)
* new LinePosition(setSelectedRange#1).startPos == position.startPos
* init'ed(new LinePosition(setSelectedRange#1).startPos)
*/
292 canvas.setSelectedRange(position);
293 }
294
295 /**
296 * Returns the type of text this click represents.
297 *
298 * @param lineInfo Line info of click.
299 *
300 * @return Click type for specified position
301 */
302 public ClickType getClickType(final LineInfo lineInfo) {
/*
P/P * Method: ClickType getClickType(LineInfo)
*
* Preconditions:
* lineInfo != null
* init'ed(lineInfo.line)
* this.canvas != null
* (soft) init'ed(lineInfo.index)
* (soft) this.canvas.document != null
* (soft) this.canvas.document.cachedLines != null
* (soft) this.canvas.document.cachedStrings != null
* (soft) this.canvas.document.lines != null
*
* Postconditions:
* return_value == One-of{&com.dmdirc.addons.ui_swing.textpane.ClickType__static_init.new ClickType(ClickType__static_init#1), &com.dmdirc.addons.ui_swing.textpane.ClickType__static_init.new ClickType(ClickType__static_init#2), &com.dmdirc.addons.ui_swing.textpane.ClickType_...
* return_value in Addr_Set{&com.dmdirc.addons.ui_swing.textpane.ClickType__static_init.new ClickType(ClickType__static_init#1),&com.dmdirc.addons.ui_swing.textpane.ClickType__static_init.new ClickType(ClickType__static_init#2),&com.dmdirc.addons.ui_swing.textpane.ClickType__static_init.new ClickType(ClickType__static_init#3),&com.dmdirc.addons.ui_swing.textpane.ClickType__static_init.new ClickType(ClickType__static_init#4)}
*/
303 return canvas.getClickType(lineInfo);
304 }
305
306 /**
307 * Returns the surrouding word at the specified position.
308 *
309 * @param lineNumber Line number to get word from
310 * @param index Position to get surrounding word
311 *
312 * @return Surrounding word
313 */
314 public String getWordAtIndex(final int lineNumber, final int index) {
/*
P/P * Method: String getWordAtIndex(int, int)
*
* Preconditions:
* (soft) this.canvas != null
* (soft) this.document != null
* (soft) this.document.lines != null
*
* Presumptions:
* com.dmdirc.ui.messages.Styliser:stipControlCodes(...)@107 != null
* getLine(...).lineParts != null
* getLine(...).lineParts.length <= 232-1
* getLine(...)@318 init'ed
* indexes.length@318 >= 2
* ...
*
* Postconditions:
* java.lang.String:substring(...)._tainted == 0
* return_value in Addr_Set{&java.lang.String:substring(...),&""}
*
* Test Vectors:
* lineNumber: {-231..-2, 0..232-1}, {-1}
*/
315 if (lineNumber == -1) {
316 return "";
317 }
318 final int[] indexes =
319 canvas.getSurroundingWordIndexes(document.getLine(lineNumber).
320 getText(),
321 index);
322 return document.getLine(lineNumber).getText().substring(indexes[0],
323 indexes[1]);
324 }
325
326 /**
327 * Returns the atrriute value for the specified location.
328 *
329 * @param lineInfo Specified location
330 *
331 * @return Specified value
332 */
333 public Object getAttributeValueAtPoint(LineInfo lineInfo) {
/*
P/P * Method: Object getAttributeValueAtPoint(LineInfo)
*
* Preconditions:
* lineInfo != null
* init'ed(lineInfo.line)
* this.canvas != null
* (soft) init'ed(lineInfo.index)
* (soft) this.canvas.document != null
* (soft) this.canvas.document.cachedLines != null
* (soft) this.canvas.document.cachedStrings != null
* (soft) this.canvas.document.lines != null
*
* Postconditions:
* init'ed(return_value)
*/
334 return canvas.getAttributeValueAtPoint(lineInfo);
335 }
336
337 /** Adds the selected text to the clipboard. */
338 public void copy() {
/*
P/P * Method: void copy()
*
* Preconditions:
* this.canvas != null
* this.canvas.selection != null
* init'ed(this.canvas.selection.endLine)
* init'ed(this.canvas.selection.endPos)
* init'ed(this.canvas.selection.startLine)
* init'ed(this.canvas.selection.startPos)
* (soft) this.document != null
* (soft) this.document.lines != null
*
* Presumptions:
* java.awt.Toolkit:getDefaultToolkit(...)@340 != null
* java.awt.Toolkit:getSystemClipboard(...)@340 != null
*
* Test Vectors:
* java.lang.String:isEmpty(...)@339: {1}, {0}
*/
339 if (getSelectedText() != null && !getSelectedText().isEmpty()) {
340 Toolkit.getDefaultToolkit().getSystemClipboard().setContents(
341 new StringSelection(getSelectedText()), null);
342 }
343 }
344
345 /** Clears the textpane. */
346 public void clear() {
/*
P/P * Method: void clear()
*
* Preconditions:
* init'ed(this.canvas.scrollBarPosition)
* this.canvas != null
* this.document != null
* this.document.lines != null
* this.document.listeners != null
* this.scrollBar != null
* (soft) this.canvas.textPane != null
*
* Postconditions:
* init'ed(this.canvas.scrollBarPosition)
*/
347 document.clear();
348 setScrollBarPosition(0);
349 setScrollBarMax(1);
350 canvas.repaint();
351 }
352
353 /** Clears the selection. */
354 public void clearSelection() {
/*
P/P * Method: void clearSelection()
*
* Preconditions:
* this.canvas != null
* this.canvas.selection != null
* init'ed(this.canvas.selection.startLine)
* init'ed(this.canvas.selection.startPos)
*
* Postconditions:
* this.canvas.selection.endLine == this.canvas.selection.startLine
* init'ed(this.canvas.selection.endLine)
* this.canvas.selection.endPos == this.canvas.selection.startPos
* init'ed(this.canvas.selection.endPos)
*/
355 canvas.clearSelection();
356 }
357
358 /**
359 * Trims the document to the specified number of lines.
360 *
361 * @param numLines Number of lines to trim the document to
362 */
363 public void trim(final int numLines) {
/*
P/P * Method: void trim(int)
*
* Preconditions:
* this.document != null
* this.document.lines != null
* (soft) this.canvas.selection != null
* (soft) this.canvas != null
* (soft) init'ed(this.canvas.selection.endLine)
* (soft) init'ed(this.canvas.selection.endPos)
* (soft) init'ed(this.canvas.selection.startLine)
* (soft) init'ed(this.canvas.selection.startPos)
* (soft) this.document.listeners != null
*
* Presumptions:
* selectedRange.endLine - (java.util.List:size(...)@78 - numLines) in {-231..232-1}
* selectedRange.startLine - (java.util.List:size(...)@78 - numLines) in {-231..232-1}
* java.util.List:size(...)@78 - numLines in {-231..232-1}
*
* Postconditions:
* this.canvas.selection == One-of{old this.canvas.selection, &new LinePosition(setSelectedRange#1)}
* this.canvas.selection != null
* new LinePosition(setSelectedRange#1) num objects <= 1
* new LinePosition(setSelectedRange#1).endLine >= 0
* init'ed(new LinePosition(setSelectedRange#1).endPos)
* new LinePosition(setSelectedRange#1).startLine >= 0
* init'ed(new LinePosition(setSelectedRange#1).startPos)
*/
364 if (document.getNumLines() < numLines) {
365 return;
366 }
367 final int trimmedLines = document.getNumLines() - numLines;
368 final LinePosition selectedRange = getSelectedRange();
369
370 selectedRange.setStartLine(selectedRange.getStartLine() - trimmedLines);
371 selectedRange.setEndLine(selectedRange.getEndLine() - trimmedLines);
372
373 if (selectedRange.getStartLine() < 0) {
374 selectedRange.setStartLine(0);
375 }
376 if (selectedRange.getEndLine() < 0) {
377 selectedRange.setEndLine(0);
378 }
379
380 setSelectedTexT(selectedRange);
381 document.trim(numLines);
382 }
383
384 /** Scrolls one page up in the textpane. */
385 public void pageDown() {
386 //setScrollBarPosition(scrollBar.getValue() + canvas.getLastVisibleLine()
387 // - canvas.getFirstVisibleLine() + 1);
388 //use this method for now, its consistent with the block unit for the scrollbar
/*
P/P * Method: void pageDown()
*
* Preconditions:
* init'ed(this.canvas.scrollBarPosition)
* this.canvas != null
* this.scrollBar != null
* (soft) this.canvas.textPane != null
*
* Presumptions:
* javax.swing.JScrollBar:getValue(...)@389 <= 4_294_967_285
*
* Postconditions:
* this.canvas.scrollBarPosition >= -2_147_483_638
*/
389 setScrollBarPosition(scrollBar.getValue() + 10);
390 }
391
392 /** Scrolls one page down in the textpane. */
393 public void pageUp() {
394 //setScrollBarPosition(canvas.getFirstVisibleLine());
395 //use this method for now, its consistent with the block unit for the scrollbar
/*
P/P * Method: void pageUp()
*
* Preconditions:
* init'ed(this.canvas.scrollBarPosition)
* this.canvas != null
* this.scrollBar != null
* (soft) this.canvas.textPane != null
*
* Presumptions:
* javax.swing.JScrollBar:getValue(...)@396 >= -2_147_483_638
*
* Postconditions:
* this.canvas.scrollBarPosition <= 4_294_967_285
*/
396 setScrollBarPosition(scrollBar.getValue() - 10);
397 }
398
399 /** {@inheritDoc}. */
400 @Override
401 public void lineAdded(final int line, final int size) {
/*
P/P * Method: void lineAdded(int, int)
*
* Preconditions:
* this.document != null
* this.document.lines != null
* this.scrollBar != null
* (soft) init'ed(this.canvas.scrollBarPosition)
* (soft) this.canvas != null
* (soft) this.canvas.textPane != null
*
* Postconditions:
* init'ed(this.canvas.scrollBarPosition)
*/
402 setScrollBarMax(1);
403 }
404
405 /** {@inheritDoc}. */
406 @Override
407 public void trimmed(final int numLines) {
/*
P/P * Method: void trimmed(int)
*
* Preconditions:
* this.canvas != null
* this.document != null
* this.document.lines != null
* this.scrollBar != null
* (soft) init'ed(this.canvas.scrollBarPosition)
* (soft) this.canvas.textPane != null
*
* Postconditions:
* init'ed(this.canvas.scrollBarPosition)
*/
408 canvas.clearWrapCache();
409 setScrollBarMax(1);
410 }
411
412 /** {@inheritDoc}. */
413 @Override
414 public void cleared() {
/*
P/P * Method: void cleared()
*
* Preconditions:
* this.canvas != null
*/
415 canvas.clearWrapCache();
416 }
417
418 /** {@inheritDoc}. */
419 @Override
420 public void linesAdded(int line, int length, int size) {
/*
P/P * Method: void linesAdded(int, int, int)
*
* Preconditions:
* this.document != null
* this.document.lines != null
* this.scrollBar != null
* (soft) init'ed(this.canvas.scrollBarPosition)
* (soft) this.canvas != null
* (soft) this.canvas.textPane != null
*
* Postconditions:
* init'ed(this.canvas.scrollBarPosition)
*/
421 setScrollBarMax(length);
422 }
423
424 /** {@inheritDoc}. */
425 @Override
426 public void repaintNeeded() {
/*
P/P * Method: void repaintNeeded()
*
* Preconditions:
* this.canvas != null
*/
427 canvas.repaint();
428 }
429
430 /**
431 * Retrieves this textpane's IRCDocument.
432 *
433 * @return This textpane's IRC document
434 */
435 public IRCDocument getDocument() {
/*
P/P * Method: IRCDocument getDocument()
*
* Postconditions:
* return_value == this.document
* init'ed(return_value)
*/
436 return document;
437 }
438
439 /**
440 * Retrives the parent framecontainer for this textpane.
441 *
442 * @return Parent frame container
443 */
444 public FrameContainer getFrameContainer() {
/*
P/P * Method: FrameContainer getFrameContainer()
*
* Postconditions:
* return_value == this.frame
* init'ed(return_value)
*/
445 return frame;
446 }
447 }
SofCheck Inspector Build Version : 2.17854
| TextPane.java |
2009-Jun-25 01:54:24 |
| TextPane.class |
2009-Sep-02 17:04:14 |
| TextPane$1.class |
2009-Sep-02 17:04:14 |