File Source: TextPaneCanvas.java
/*
P/P * Method: com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas$1__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.addons.ui_swing.UIUtilities;
26 import com.dmdirc.interfaces.ConfigChangeListener;
27 import com.dmdirc.ui.messages.IRCTextAttribute;
28
29 import java.awt.Cursor;
30 import java.awt.Graphics;
31 import java.awt.Graphics2D;
32 import java.awt.Point;
33 import java.awt.Rectangle;
34 import java.awt.Shape;
35 import java.awt.Toolkit;
36 import java.awt.event.ComponentEvent;
37 import java.awt.event.ComponentListener;
38 import java.awt.event.MouseEvent;
39 import java.awt.font.LineBreakMeasurer;
40 import java.awt.font.TextAttribute;
41 import java.awt.font.TextHitInfo;
42 import java.awt.font.TextLayout;
43 import java.text.AttributedCharacterIterator;
44 import java.text.AttributedString;
45 import java.util.HashMap;
46 import java.util.Map;
47
48 import javax.swing.JPanel;
49 import javax.swing.SwingUtilities;
50 import javax.swing.event.MouseInputListener;
51
52 /** Canvas object to draw text. */
/*
P/P * Method: Map access$000(TextPaneCanvas)
*
* Preconditions:
* x0 != null
*
* Postconditions:
* return_value == x0.lineWrap
* init'ed(return_value)
*/
53 class TextPaneCanvas extends JPanel implements MouseInputListener,
54 ComponentListener, ConfigChangeListener {
55
56 /**
57 * A version number for this class. It should be changed whenever the
58 * class structure is changed (or anything else that would prevent
59 * serialized objects being unserialized with the new class).
60 */
61 private static final long serialVersionUID = 8;
62 /** Hand cursor. */
/*
P/P * Method: com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas__static_init
*
* Postconditions:
* HAND_CURSOR == &new Cursor(TextPaneCanvas__static_init#1)
* new Cursor(TextPaneCanvas__static_init#1) num objects == 1
*/
63 private static final Cursor HAND_CURSOR = new Cursor(Cursor.HAND_CURSOR);
64 /** IRCDocument. */
65 private final IRCDocument document;
66 /** parent textpane. */
67 private final TextPane textPane;
68 /** Position -> TextLayout. */
69 private final Map<Rectangle, TextLayout> positions;
70 /** TextLayout -> Line numbers. */
71 private final Map<TextLayout, LineInfo> textLayouts;
72 /** position of the scrollbar. */
73 private int scrollBarPosition;
74 /** Selection. */
75 private LinePosition selection;
76 /** First visible line. */
77 private int firstVisibleLine;
78 /** Last visible line. */
79 private int lastVisibleLine;
80 /** Line wrapping cache. */
81 private final Map<Integer, Integer> lineWrap;
82
83 /**
84 * Creates a new text pane canvas.
85 *
86 * @param parent parent text pane for the canvas
87 * @param document IRCDocument to be displayed
88 */
89 public TextPaneCanvas(final TextPane parent, final IRCDocument document) {
/*
P/P * Method: void com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas(TextPane, IRCDocument)
*
* Postconditions:
* this.document == document
* init'ed(this.document)
* this.lineWrap == &new HashMap(TextPaneCanvas#3)
* this.positions == &new HashMap(TextPaneCanvas#2)
* init'ed(this.scrollBarPosition)
* this.selection == &new LinePosition(TextPaneCanvas#4)
* this.textLayouts == &new HashMap(TextPaneCanvas#1)
* this.textPane == parent
* init'ed(this.textPane)
* new HashMap(TextPaneCanvas#1) num objects == 1
* ...
*/
90 super();
91 this.document = document;
92 scrollBarPosition = 0;
93 textPane = parent;
94 setDoubleBuffered(true);
95 setOpaque(true);
96 textLayouts = new HashMap<TextLayout, LineInfo>();
97 positions = new HashMap<Rectangle, TextLayout>();
98 lineWrap = new HashMap<Integer, Integer>();
99 selection = new LinePosition(-1, -1, -1, -1);
100 addMouseListener(this);
101 addMouseMotionListener(this);
102 addComponentListener(this);
103 //TODO issue 2251
104 //parent.getFrameContainer().getConfigManager().addChangeListener("ui", "textPaneFontSize", this);
105 }
106
107 /**
108 * Paints the text onto the canvas.
109 *
110 * @param graphics graphics object to draw onto
111 */
112 @Override
113 public void paintComponent(final Graphics graphics) {
/*
P/P * Method: void paintComponent(Graphics)
*
* Preconditions:
* graphics != null
* this.document != null
* this.document.lines != null
* this.positions != null
* init'ed(this.scrollBarPosition)
* this.textLayouts != null
* this.textPane != null
* (soft) this.document.cachedLines != null
* (soft) this.document.cachedStrings != null
* (soft) this.lineWrap != null
* ...
*
* Presumptions:
* (int) ((float) (com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas:getWidth(...)@122 - 6)) in {-2_147_483_654..4_294_967_289}
* (int) ((float) (getLine(...).lineHeight)*21_617_278_211_378_381/18_014_398_509_481_984) in {-231..232-1}
* java.awt.Toolkit:getDefaultToolkit(...)@116 != null
* java.awt.font.LineBreakMeasurer:nextLayout(...)@191 != null
* java.text.AttributedString:getIterator(...)@253 != null
* ...
*
* Postconditions:
* possibly_updated(this.firstVisibleLine)
* possibly_updated(this.lastVisibleLine)
*
* Test Vectors:
* java.awt.Toolkit:getDesktopProperty(...)@116: Addr_Set{null}, Inverse{null}
* java.awt.font.TextLayout:isLeftToRight(...)@201: {0}, {1}
* java.util.List:size(...)@78: {0}, {-231..-1, 1..232-1}
* java.util.Map:containsKey(...)@172: {0}, {1}
*/
114 final Graphics2D g = (Graphics2D) graphics;
115
116 final Map desktopHints = (Map) Toolkit.getDefaultToolkit().
117 getDesktopProperty("awt.font.desktophints");
118 if (desktopHints != null) {
119 g.addRenderingHints(desktopHints);
120 }
121
122 final float formatWidth = getWidth() - 6;
123 final float formatHeight = getHeight();
124 float drawPosY = formatHeight;
125 int startLine = scrollBarPosition;
126
127 int paragraphStart;
128 int paragraphEnd;
129 LineBreakMeasurer lineMeasurer;
130
131 g.setColor(textPane.getBackground());
132 g.fill(g.getClipBounds());
133
134 textLayouts.clear();
135 positions.clear();
136
137 //check theres something to draw and theres some space to draw in
138 if (document.getNumLines() == 0 || formatWidth < 1) {
139 setCursor(Cursor.getDefaultCursor());
140 return;
141 }
142
143 // Check the start line is in range
144 if (startLine >= document.getNumLines()) {
145 startLine = document.getNumLines() - 1;
146 }
147
148 if (startLine <= 0) {
149 startLine = 0;
150 }
151
152 //sets the last visible line
153 lastVisibleLine = startLine;
154 firstVisibleLine = startLine;
155
156 // Iterate through the lines
157 for (int i = startLine; i >= 0; i--) {
158 float drawPosX;
159 final AttributedCharacterIterator iterator = document.getStyledLine(
160 i);
161 int lineHeight = document.getLineHeight(i);
162 lineHeight += lineHeight * 0.2;
163 paragraphStart = iterator.getBeginIndex();
164 paragraphEnd = iterator.getEndIndex();
165 lineMeasurer = new LineBreakMeasurer(iterator,
166 g.getFontRenderContext());
167 lineMeasurer.setPosition(paragraphStart);
168
169 final int wrappedLine;
170
171 //do we have the line wrapping in the cache?
172 if (lineWrap.containsKey(i)) {
173 //use it
174 wrappedLine = lineWrap.get(i);
175 } else {
176 //get it and populate the cache
177 wrappedLine = getNumWrappedLines(lineMeasurer,
178 paragraphStart, paragraphEnd,
179 formatWidth);
180 lineWrap.put(i, wrappedLine);
181 }
182
183 if (wrappedLine > 1) {
184 drawPosY -= lineHeight * wrappedLine;
185 }
186
187 int j = 0;
188 int chars = 0;
189 // Loop through each wrapped line
190 while (lineMeasurer.getPosition() < paragraphEnd) {
191 final TextLayout layout = lineMeasurer.nextLayout(formatWidth);
192
193 // Calculate the Y offset
194 if (wrappedLine == 1) {
195 drawPosY -= lineHeight;
196 } else if (j != 0) {
197 drawPosY += lineHeight;
198 }
199
200 // Calculate the initial X position
201 if (layout.isLeftToRight()) {
202 drawPosX = 3;
203 } else {
204 drawPosX = formatWidth - layout.getAdvance();
205 }
206
207 // Check if the target is in range
208 if (drawPosY >= 0 || drawPosY <= formatHeight) {
209
210 g.setColor(textPane.getForeground());
211
212 layout.draw(g, drawPosX, drawPosY + lineHeight / 2f);
213 doHighlight(i, chars, layout, g, drawPosY, drawPosX);
214 firstVisibleLine = i;
215 textLayouts.put(layout, new LineInfo(i, j));
216 positions.put(new Rectangle(0, (int) drawPosY,
217 (int) formatWidth + 6,
218 lineHeight), layout);
219 }
220
221 j++;
222 chars += layout.getCharacterCount();
223 }
224 if (j > 1) {
225 drawPosY -= lineHeight * (wrappedLine - 1);
226 }
227 if (drawPosY <= 0) {
228 break;
229 }
230 }
231 checkForLink();
232 }
233
234 /**
235 * Returns the number of timesa line will wrap.
236 *
237 * @param lineMeasurer LineBreakMeasurer to work out wrapping for
238 * @param paragraphStart Start index of the paragraph
239 * @param paragraphEnd End index of the paragraph
240 * @param formatWidth Width to wrap at
241 *
242 * @return Number of times the line wraps
243 */
244 private int getNumWrappedLines(final LineBreakMeasurer lineMeasurer,
245 final int paragraphStart,
246 final int paragraphEnd,
247 final float formatWidth) {
/*
P/P * Method: int getNumWrappedLines(LineBreakMeasurer, int, int, float)
*
* Preconditions:
* lineMeasurer != null
*
* Postconditions:
* return_value >= 0
*/
248 int wrappedLine = 0;
249
250 while (lineMeasurer.getPosition() < paragraphEnd) {
251 lineMeasurer.nextLayout(formatWidth);
252
253 wrappedLine++;
254 }
255
256 lineMeasurer.setPosition(paragraphStart);
257
258 return wrappedLine;
259 }
260
261 /**
262 * Redraws the text that has been highlighted.
263 *
264 * @param line Line number
265 * @param chars Number of characters so far in the line
266 * @param layout Current line textlayout
267 * @param g Graphics surface to draw highlight on
268 * @param drawPosY current y location of the line
269 * @param drawPosX current x location of the line
270 */
271 private void doHighlight(final int line, final int chars,
272 final TextLayout layout, final Graphics2D g,
273 final float drawPosY, final float drawPosX) {
274 int startLine;
275 int startChar;
276 int endLine;
277 int endChar;
278
/*
P/P * Method: void doHighlight(int, int, TextLayout, Graphics2D, float, float)
*
* Preconditions:
* this.selection != null
* init'ed(this.selection.endLine)
* init'ed(this.selection.endPos)
* init'ed(this.selection.startLine)
* init'ed(this.selection.startPos)
* (soft) g != null
* (soft) layout != null
* (soft) this.document != null
* (soft) this.document.cachedLines != null
* (soft) this.document.cachedStrings != null
* ...
*
* Presumptions:
* (int) ((float) (getLine(...).lineHeight)*21_617_278_211_378_381/18_014_398_509_481_984) in {-231..232-1}
* (int) ((float) (getLineHeight(...)@333)*21_617_278_211_378_381/18_014_398_509_481_984) in range
* (int) (drawPosY + (float) ((int) ((float) (getLine(...).lineHeight)*21_617_278_211_378_381/18_014_398_509_481_984))/2) in {-231..232-1}
* (int) (drawPosY + (float) ((int) ((float) (getLineHeight(...)@333)*21_617_278_211_378_381/18_014_398_509_481_984))/2) in range
* chars + java.awt.font.TextLayout:getCharacterCount(...)@314 in {-231..232-1}
* ...
*
* Test Vectors:
* this.selection.endLine - this.selection.startLine: {1..6_442_450_943}, {-6_442_450_943..-1}, {0}
* this.selection.endPos - this.selection.startPos: {0..6_442_450_943}, {-6_442_450_943..-1}
* java.lang.String:isEmpty(...)@327: {0}, {1}
*/
279 if (selection.getStartLine() > selection.getEndLine()) {
280 // Swap both
281 startLine = selection.getEndLine();
282 startChar = selection.getEndPos();
283 endLine = selection.getStartLine();
284 endChar = selection.getStartPos();
285 } else if (selection.getStartLine() == selection.getEndLine() &&
286 selection.getStartPos() > selection.getEndPos()) {
287 // Just swap the chars
288 startLine = selection.getStartLine();
289 startChar = selection.getEndPos();
290 endLine = selection.getEndLine();
291 endChar = selection.getStartPos();
292 } else {
293 // Swap nothing
294 startLine = selection.getStartLine();
295 startChar = selection.getStartPos();
296 endLine = selection.getEndLine();
297 endChar = selection.getEndPos();
298 }
299
300 //Does this line need highlighting?
301 if (startLine <= line && endLine >= line) {
302 int firstChar;
303 int lastChar;
304
305 // Determine the first char we care about
306 if (startLine < line || startChar < chars) {
307 firstChar = chars;
308 } else {
309 firstChar = startChar;
310 }
311
312 // ... And the last
313 if (endLine > line || endChar > chars + layout.getCharacterCount()) {
314 lastChar = chars + layout.getCharacterCount();
315 } else {
316 lastChar = endChar;
317 }
318
319 // If the selection includes the chars we're showing
320 if (lastChar > chars && firstChar < chars +
321 layout.getCharacterCount()) {
322 String text = document.getLine(line).getText();
323 if (firstChar >= 0 && text.length() > lastChar) {
324 text = text.substring(firstChar, lastChar);
325 }
326
327 if (text.isEmpty()) {
328 return;
329 }
330
331 final AttributedCharacterIterator iterator = document.
332 getStyledLine(line);
333 int lineHeight = document.getLineHeight(line);
334 lineHeight += lineHeight * 0.2;
335 final AttributedString as = new AttributedString(iterator,
336 firstChar,
337 lastChar);
338 final int trans = (int) (lineHeight / 2f + drawPosY);
339
340 as.addAttribute(TextAttribute.FOREGROUND,
341 textPane.getBackground());
342 as.addAttribute(TextAttribute.BACKGROUND,
343 textPane.getForeground());
344 final TextLayout newLayout = new TextLayout(as.getIterator(),
345 g.getFontRenderContext());
346 final Shape shape = layout.getLogicalHighlightShape(firstChar -
347 chars,
348 lastChar -
349 chars);
350
351 if (firstChar != 0) {
352 g.translate(shape.getBounds().getX(), 0);
353 }
354
355 newLayout.draw(g, drawPosX, trans);
356
357 if (firstChar != 0) {
358 g.translate(-1 * shape.getBounds().getX(), 0);
359 }
360 }
361 }
362 }
363
364 /**
365 * sets the position of the scroll bar, and repaints if required.
366 * @param position scroll bar position
367 */
368 protected void setScrollBarPosition(final int position) {
/*
P/P * Method: void setScrollBarPosition(int)
*
* Preconditions:
* init'ed(this.scrollBarPosition)
* (soft) this.textPane != null
*
* Postconditions:
* this.scrollBarPosition == One-of{old this.scrollBarPosition, position}
* init'ed(this.scrollBarPosition)
*
* Test Vectors:
* this.scrollBarPosition - position: {0}, {-6_442_450_943..-1, 1..6_442_450_943}
* com.dmdirc.addons.ui_swing.textpane.TextPane:isVisible(...)@371: {0}, {1}
*/
369 if (scrollBarPosition != position) {
370 scrollBarPosition = position;
371 if (textPane.isVisible()) {
372 repaint();
373 }
374 }
375 }
376
377 /**
378 * Returns the current scroll bar position.
379 *
380 * @return Scroll bar position
381 */
382 protected int getScrollBarPosition() {
/*
P/P * Method: int getScrollBarPosition()
*
* Preconditions:
* init'ed(this.scrollBarPosition)
*
* Postconditions:
* return_value == this.scrollBarPosition
* init'ed(return_value)
*/
383 return scrollBarPosition;
384 }
385
386 /**
387 * {@inheritDoc}
388 *
389 * @param e Mouse event
390 */
391 @Override
392 public void mouseClicked(final MouseEvent e) {
/*
P/P * Method: void mouseClicked(MouseEvent)
*
* Preconditions:
* e != null
* this.textPane != null
* (soft) this.document != null
* (soft) this.document.lines != null
* (soft) this.positions != null
* (soft) this.selection != null
* (soft) this.textLayouts != null
*
* Presumptions:
* com.dmdirc.ui.messages.Styliser:stipControlCodes(...)@107 != null
* extent.length@406 >= 2
* getLine(...).lineParts != null
* getLine(...).lineParts.length <= 232-1
* getLine(...)@400 init'ed
* ...
*
* Postconditions:
* possibly_updated(this.selection.endLine)
* possibly_updated(this.selection.endPos)
* possibly_updated(this.selection.startLine)
* possibly_updated(this.selection.startPos)
*
* Test Vectors:
* java.awt.event.MouseEvent:getClickCount(...)@413: {-231..1, 3..232-1}, {2}
* java.awt.event.MouseEvent:getClickCount(...)@418: {-231..2, 4..232-1}, {3}
*/
393 String clickedText = "";
394 final int start;
395 final int end;
396
397 final LineInfo lineInfo = getClickPosition(getMousePosition());
398
399 if (lineInfo.getLine() != -1) {
400 clickedText = document.getLine(lineInfo.getLine()).getText();
401
402 if (lineInfo.getIndex() == -1) {
403 start = -1;
404 end = -1;
405 } else {
406 final int[] extent =
407 getSurroundingWordIndexes(clickedText,
408 lineInfo.getIndex());
409 start = extent[0];
410 end = extent[1];
411 }
412
413 if (e.getClickCount() == 2) {
414 selection.setStartLine(lineInfo.getLine());
415 selection.setEndLine(lineInfo.getLine());
416 selection.setStartPos(start);
417 selection.setEndPos(end);
418 } else if (e.getClickCount() == 3) {
419 selection.setStartLine(lineInfo.getLine());
420 selection.setEndLine(lineInfo.getLine());
421 selection.setStartPos(0);
422 selection.setEndPos(clickedText.length());
423 }
424 }
425
426 e.setSource(textPane);
427 textPane.dispatchEvent(e);
428 }
429
430 /**
431 * Returns the type of text this click represents.
432 *
433 * @param lineInfo Line info of click.
434 *
435 * @return Click type for specified position
436 */
437 public ClickType getClickType(final LineInfo lineInfo) {
/*
P/P * Method: ClickType getClickType(LineInfo)
*
* Preconditions:
* lineInfo != null
* init'ed(lineInfo.line)
* (soft) init'ed(lineInfo.index)
* (soft) this.document != null
* (soft) this.document.cachedLines != null
* (soft) this.document.cachedStrings != null
* (soft) this.document.lines != null
*
* Presumptions:
* init'ed(com.dmdirc.ui.messages.IRCTextAttribute.CHANNEL)
* init'ed(com.dmdirc.ui.messages.IRCTextAttribute.HYPERLINK)
* init'ed(com.dmdirc.ui.messages.IRCTextAttribute.NICKNAME)
* getStyledLine(...)@439 init'ed
* java.text.AttributedCharacterIterator:getAttributes(...)@444 != null
* ...
*
* Postconditions:
* return_value in Addr_Set{&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#2),&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#4)}
*
* Test Vectors:
* lineInfo.line: {-1}, {-231..-2, 0..232-1}
*/
438 if (lineInfo.getLine() != -1) {
439 final AttributedCharacterIterator iterator = document.getStyledLine(
440 lineInfo.getLine());
441 final int index = lineInfo.getIndex();
442 if (index >= iterator.getBeginIndex() && index <= iterator.getEndIndex()) {
443 iterator.setIndex(lineInfo.getIndex());
444 Object linkattr =
445 iterator.getAttributes().get(IRCTextAttribute.HYPERLINK);
446 if (linkattr instanceof String) {
447 return ClickType.HYPERLINK;
448 }
449 linkattr =
450 iterator.getAttributes().get(IRCTextAttribute.CHANNEL);
451 if (linkattr instanceof String) {
452 return ClickType.CHANNEL;
453 }
454 linkattr = iterator.getAttributes().get(
455 IRCTextAttribute.NICKNAME);
456 if (linkattr instanceof String) {
457 return ClickType.NICKNAME;
458 }
459 } else {
460 return ClickType.NORMAL;
461 }
462 }
463 return ClickType.NORMAL;
464 }
465
466 /**
467 * Returns the atrriute value for the specified location.
468 *
469 * @param lineInfo Specified location
470 *
471 * @return Specified value
472 */
473 public Object getAttributeValueAtPoint(LineInfo lineInfo) {
/*
P/P * Method: Object getAttributeValueAtPoint(LineInfo)
*
* Preconditions:
* lineInfo != null
* init'ed(lineInfo.line)
* (soft) init'ed(lineInfo.index)
* (soft) this.document != null
* (soft) this.document.cachedLines != null
* (soft) this.document.cachedStrings != null
* (soft) this.document.lines != null
*
* Presumptions:
* init'ed(com.dmdirc.ui.messages.IRCTextAttribute.CHANNEL)
* init'ed(com.dmdirc.ui.messages.IRCTextAttribute.HYPERLINK)
* init'ed(com.dmdirc.ui.messages.IRCTextAttribute.NICKNAME)
* getStyledLine(...)@475 init'ed
* java.text.AttributedCharacterIterator:getAttributes(...)@478 != null
* ...
*
* Postconditions:
* init'ed(return_value)
*
* Test Vectors:
* lineInfo.line: {-1}, {-231..-2, 0..232-1}
*/
474 if (lineInfo.getLine() != -1) {
475 final AttributedCharacterIterator iterator = document.getStyledLine(
476 lineInfo.getLine());
477 iterator.setIndex(lineInfo.getIndex());
478 Object linkattr =
479 iterator.getAttributes().get(IRCTextAttribute.HYPERLINK);
480 if (linkattr instanceof String) {
481 return linkattr;
482 }
483 linkattr = iterator.getAttributes().get(IRCTextAttribute.CHANNEL);
484 if (linkattr instanceof String) {
485 return linkattr;
486 }
487 linkattr = iterator.getAttributes().get(IRCTextAttribute.NICKNAME);
488 if (linkattr instanceof String) {
489 return linkattr;
490 }
491 }
492 return null;
493 }
494
495 /**
496 * Returns the indexes for the word surrounding the index in the specified
497 * string.
498 *
499 * @param text Text to get word from
500 * @param index Index to get surrounding word
501 *
502 * @return Indexes of the word surrounding the index (start, end)
503 */
504 protected int[] getSurroundingWordIndexes(final String text,
505 final int index) {
/*
P/P * Method: int[] getSurroundingWordIndexes(String, int)
*
* Preconditions:
* text != null
*
* Postconditions:
* return_value in Addr_Set{&new int[](getSurroundingWordIndexes#2),&new int[](getSurroundingWordIndexes#1)}
* new int[](getSurroundingWordIndexes#1) num objects <= 1
* new int[](getSurroundingWordIndexes#1).length == 2
* new int[](getSurroundingWordIndexes#1)[0] == 0
* new int[](getSurroundingWordIndexes#1)[1] == 0
* new int[](getSurroundingWordIndexes#2) num objects <= 1
* new int[](getSurroundingWordIndexes#2).length == 2
* new int[](getSurroundingWordIndexes#2)[0] >= 0
* new int[](getSurroundingWordIndexes#2)[1] >= 0
*/
506 final int start = getSurroundingWordStart(text, index);
507 final int end = getSurroundingWordEnd(text, index);
508
509 if (start < 0 || end > text.length() || start > end) {
510 return new int[]{0, 0};
511 }
512
513 return new int[]{start, end};
514
515 }
516
517 /**
518 * Returns the start index for the word surrounding the index in the
519 * specified string.
520 *
521 * @param text Text to get word from
522 * @param index Index to get surrounding word
523 *
524 * @return Start index of the word surrounding the index
525 */
526 private int getSurroundingWordStart(final String text, final int index) {
/*
P/P * Method: int getSurroundingWordStart(String, int)
*
* Preconditions:
* text != null
*
* Postconditions:
* init'ed(return_value)
*
* Test Vectors:
* java.lang.String:charAt(...)@530: {32}, {0..31, 33..216-1}
* java.lang.String:charAt(...)@533: {0..31, 33..216-1}, {32}
*/
527 int start = index;
528
529 // Traverse backwards
530 while (start > 0 && start < text.length() && text.charAt(start) != ' ') {
531 start--;
532 }
533 if (start + 1 < text.length() && text.charAt(start) == ' ') {
534 start++;
535 }
536
537 return start;
538 }
539
540 /**
541 * Returns the end index for the word surrounding the index in the
542 * specified string.
543 *
544 * @param text Text to get word from
545 * @param index Index to get surrounding word
546 *
547 * @return End index of the word surrounding the index
548 */
549 private int getSurroundingWordEnd(final String text, final int index) {
/*
P/P * Method: int getSurroundingWordEnd(String, int)
*
* Preconditions:
* text != null
*
* Postconditions:
* init'ed(return_value)
* return_value - index in {0..6_442_450_943}
*
* Test Vectors:
* java.lang.String:charAt(...)@553: {32}, {0..31, 33..216-1}
*/
550 int end = index;
551
552 // And forwards
553 while (end < text.length() && end > 0 && text.charAt(end) != ' ') {
554 end++;
555 }
556
557 return end;
558 }
559
560 /**
561 * {@inheritDoc}
562 *
563 * @param e Mouse event
564 */
565 @Override
566 public void mousePressed(final MouseEvent e) {
/*
P/P * Method: void mousePressed(MouseEvent)
*
* Preconditions:
* e != null
* this.textPane != null
* (soft) this.positions != null
* (soft) this.selection != null
* (soft) this.textLayouts != null
*
* Postconditions:
* possibly_updated(this.selection.endLine)
* possibly_updated(this.selection.endPos)
* possibly_updated(this.selection.startLine)
* possibly_updated(this.selection.startPos)
*
* Test Vectors:
* java.awt.event.MouseEvent:getButton(...)@567: {-231..0, 2..232-1}, {1}
*/
567 if (e.getButton() == MouseEvent.BUTTON1) {
568 highlightEvent(MouseEventType.CLICK, e);
569 }
570 e.setSource(textPane);
571 textPane.dispatchEvent(e);
572 }
573
574 /**
575 * {@inheritDoc}
576 *
577 * @param e Mouse event
578 */
579 @Override
580 public void mouseReleased(final MouseEvent e) {
/*
P/P * Method: void mouseReleased(MouseEvent)
*
* Preconditions:
* e != null
* this.textPane != null
* (soft) this.positions != null
* (soft) this.selection != null
* (soft) this.textLayouts != null
*
* Postconditions:
* possibly_updated(this.selection.endLine)
* possibly_updated(this.selection.endPos)
* possibly_updated(this.selection.startLine)
* possibly_updated(this.selection.startPos)
*
* Test Vectors:
* java.awt.event.MouseEvent:getButton(...)@581: {-231..0, 2..232-1}, {1}
*/
581 if (e.getButton() == MouseEvent.BUTTON1) {
582 highlightEvent(MouseEventType.RELEASE, e);
583 }
584 e.setSource(textPane);
585 textPane.dispatchEvent(e);
586 }
587
588 /**
589 * {@inheritDoc}
590 *
591 * @param e Mouse event
592 */
593 @Override
594 public void mouseDragged(final MouseEvent e) {
/*
P/P * Method: void mouseDragged(MouseEvent)
*
* Preconditions:
* e != null
* this.textPane != null
* (soft) this.positions != null
* (soft) this.selection != null
* (soft) this.textLayouts != null
*
* Postconditions:
* possibly_updated(this.selection.endLine)
* possibly_updated(this.selection.endPos)
* possibly_updated(this.selection.startLine)
* possibly_updated(this.selection.startPos)
*
* Test Vectors:
* java.awt.event.MouseEvent:getModifiersEx(...)@595: {-231..1_023, 1_025..232-1}, {1_024}
*/
595 if (e.getModifiersEx() == MouseEvent.BUTTON1_DOWN_MASK) {
596 highlightEvent(MouseEventType.DRAG, e);
597 }
598
599 e.setSource(textPane);
600 textPane.dispatchEvent(e);
601 }
602
603 /**
604 * {@inheritDoc}
605 *
606 * @param e Mouse event
607 */
608 @Override
609 public void mouseEntered(final MouseEvent e) {
610 //Ignore
/*
P/P * Method: void mouseEntered(MouseEvent)
*/
611 }
612
613 /**
614 * {@inheritDoc}
615 *
616 * @param e Mouse event
617 */
618 @Override
619 public void mouseExited(final MouseEvent e) {
620 //Ignore
/*
P/P * Method: void mouseExited(MouseEvent)
*/
621 }
622
623 /**
624 * {@inheritDoc}
625 *
626 * @param e Mouse event
627 */
628 @Override
629 public void mouseMoved(final MouseEvent e) {
/*
P/P * Method: void mouseMoved(MouseEvent)
*
* Preconditions:
* (soft) this.document != null
* (soft) this.document.cachedLines != null
* (soft) this.document.cachedStrings != null
* (soft) this.document.lines != null
* (soft) this.positions != null
* (soft) this.textLayouts != null
*/
630 checkForLink();
631 }
632
633 /** Checks for a link under the cursor and sets appropriately. */
634 private void checkForLink() {
/*
P/P * Method: void checkForLink()
*
* Preconditions:
* (soft) this.document != null
* (soft) this.document.cachedLines != null
* (soft) this.document.cachedStrings != null
* (soft) this.document.lines != null
* (soft) this.positions != null
* (soft) this.textLayouts != null
*
* Presumptions:
* init'ed(com.dmdirc.ui.messages.IRCTextAttribute.CHANNEL)
* init'ed(com.dmdirc.ui.messages.IRCTextAttribute.HYPERLINK)
* init'ed(com.dmdirc.ui.messages.IRCTextAttribute.NICKNAME)
* java.text.AttributedCharacterIterator:getAttributes(...)@646 != null
* java.text.AttributedCharacterIterator:getAttributes(...)@652 != null
* ...
*
* Test Vectors:
* com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas:getCursor(...)@663: Inverse{&new Cursor(TextPaneCanvas__static_init#1)}, Addr_Set{&new Cursor(TextPaneCanvas__static_init#1)}
* java.util.List:get(...)@89: Addr_Set{null}, Inverse{null}
*/
635 final LineInfo lineInfo = getClickPosition(getMousePosition());
636
637 if (lineInfo.getLine() != -1 && document.getLine(lineInfo.getLine()) !=
638 null) {
639 final AttributedCharacterIterator iterator = document.getStyledLine(
640 lineInfo.getLine());
641 if (lineInfo.getIndex() < iterator.getBeginIndex() ||
642 lineInfo.getIndex() > iterator.getEndIndex()) {
643 return;
644 }
645 iterator.setIndex(lineInfo.getIndex());
646 Object linkattr =
647 iterator.getAttributes().get(IRCTextAttribute.HYPERLINK);
648 if (linkattr instanceof String) {
649 setCursor(HAND_CURSOR);
650 return;
651 }
652 linkattr = iterator.getAttributes().get(IRCTextAttribute.CHANNEL);
653 if (linkattr instanceof String) {
654 setCursor(HAND_CURSOR);
655 return;
656 }
657 linkattr = iterator.getAttributes().get(IRCTextAttribute.NICKNAME);
658 if (linkattr instanceof String) {
659 setCursor(HAND_CURSOR);
660 return;
661 }
662 }
663 if (getCursor() == HAND_CURSOR) {
664 setCursor(Cursor.getDefaultCursor());
665 }
666 }
667
668 /**
669 * Sets the selection for the given event.
670 *
671 * @param type mouse event type
672 * @param e responsible mouse event
673 */
674 protected void highlightEvent(final MouseEventType type,
675 final MouseEvent e) {
/*
P/P * Method: void highlightEvent(MouseEventType, MouseEvent)
*
* Preconditions:
* (soft) e != null
* (soft) this.positions != null
* (soft) this.selection != null
* (soft) this.textLayouts != null
*
* Presumptions:
* com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas:getBounds(...)@680 != null
* java.awt.event.MouseEvent:getLocationOnScreen(...)@677 != null
* java.awt.event.MouseEvent:getPoint(...)@681 != null
*
* Postconditions:
* possibly_updated(this.selection.endLine)
* possibly_updated(this.selection.endPos)
* possibly_updated(this.selection.startLine)
* possibly_updated(this.selection.startPos)
*
* Test Vectors:
* com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas:contains(...)@679: {1}, {0}
* com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas:contains(...)@701: {0}, {1}
* com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas:isVisible(...)@676: {0}, {1}
*/
676 if (isVisible()) {
677 Point point = e.getLocationOnScreen();
678 SwingUtilities.convertPointFromScreen(point, this);
679 if (!contains(point)) {
680 final Rectangle bounds = getBounds();
681 final Point mousePos = e.getPoint();
682 if (mousePos.getX() < bounds.getX()) {
683 point.setLocation(bounds.getX() + 3, point.getY());
684 } else if (mousePos.getX() > (bounds.getX() + bounds.getWidth())) {
685 point.setLocation(bounds.getX() + bounds.getWidth() - 3,
686 point.getY());
687 }
688 if (mousePos.getY() < bounds.getY()) {
689 point.setLocation(point.getX(), bounds.getY() + 6);
690 } else if (mousePos.getY() >
691 (bounds.getY() + bounds.getHeight())) {
692 //Nice text selection behaviour
693 //point.setLocation(point.getX(), bounds.getY() +
694 // bounds.getHeight() - 6);
695 point.setLocation(bounds.getX() + bounds.getWidth() - 3,
696 bounds.getY() +
697 bounds.getHeight() - 6);
698 }
699 }
700 final LineInfo info = getClickPosition(point);
701 if (info.getLine() == -1 && info.getPart() == -1 && contains(point)) {
702 info.setLine(0);
703 info.setPart(0);
704 //Nice text selection behaviour
705 //info.setIndex(getHitPosition(info.getLine(), info.getPart(),
706 // point.x, 0));
707 info.setIndex(0);
708 }
709 if (info.getLine() != -1 && info.getPart() != -1) {
710 if (type == MouseEventType.CLICK) {
711 selection.setStartLine(info.getLine());
712 selection.setStartPos(info.getIndex());
713 }
714 selection.setEndLine(info.getLine());
715 selection.setEndPos(info.getIndex());
716
717 repaint();
718 }
719 }
720 }
721
722 /**
723 *
724 * Returns the line information from a mouse click inside the textpane.
725 *
726 * @param point mouse position
727 *
728 * @return line number, line part, position in whole line
729 */
730 public LineInfo getClickPosition(final Point point) {
/*
P/P * Method: LineInfo getClickPosition(Point)
*
* Preconditions:
* (soft) this.positions != null
* (soft) this.textLayouts != null
*
* Presumptions:
* (int) (java.awt.Point:getX(...)@743) in {-231..232-1}
* (int) (java.awt.Point:getY(...)@743) in {-231..232-1}
* java.util.Iterator:next(...)@736 != null
* java.util.Map:entrySet(...)@736 != null
* java.util.Map:get(...)@738 != null
* ...
*
* Postconditions:
* return_value == &new LineInfo(getClickPosition#1)
* new LineInfo(getClickPosition#1) num objects == 1
* init'ed(return_value.index)
* init'ed(return_value.line)
* init'ed(return_value.part)
*
* Test Vectors:
* point: Addr_Set{null}, Inverse{null}
* java.awt.Rectangle:contains(...)@737: {0}, {1}
* java.util.Iterator:hasNext(...)@736: {0}, {1}
*/
731 int lineNumber = -1;
732 int linePart = -1;
733 int pos = 0;
734
735 if (point != null) {
736 for (Map.Entry<Rectangle, TextLayout> entry : positions.entrySet()) {
737 if (entry.getKey().contains(point)) {
738 lineNumber = textLayouts.get(entry.getValue()).getLine();
739 linePart = textLayouts.get(entry.getValue()).getPart();
740 }
741 }
742
743 pos = getHitPosition(lineNumber, linePart, (int) point.getX(),
744 (int) point.getY());
745 }
746
747 return new LineInfo(lineNumber, linePart, pos);
748 }
749
750 /**
751 * Returns the character index for a specified line and part for a specific hit position.
752 *
753 * @param lineNumber Line number
754 * @param linePart Line part
755 * @param x X position
756 * @param y Y position
757 *
758 * @return Hit position
759 */
760 private int getHitPosition(final int lineNumber, final int linePart,
761 final int x, final int y) {
/*
P/P * Method: int getHitPosition(int, int, int, int)
*
* Preconditions:
* this.positions != null
* (soft) this.textLayouts != null
*
* Presumptions:
* java.awt.font.TextLayout:hitTestChar(...)@770 != null
* java.util.Iterator:next(...)@764 != null
* java.util.Map:entrySet(...)@764 != null
* java.util.Map:get(...)@765 != null
* java.util.Map:get(...)@766 != null
* ...
*
* Postconditions:
* init'ed(return_value)
*
* Test Vectors:
* java.util.Iterator:hasNext(...)@764: {0}, {1}
*/
762 int pos = 0;
763
764 for (Map.Entry<Rectangle, TextLayout> entry : positions.entrySet()) {
765 if (textLayouts.get(entry.getValue()).getLine() == lineNumber) {
766 if (textLayouts.get(entry.getValue()).getPart() < linePart) {
767 pos += entry.getValue().getCharacterCount();
768 } else if (textLayouts.get(entry.getValue()).getPart() ==
769 linePart) {
770 final TextHitInfo hit = entry.getValue().hitTestChar(x - 6,
771 y);
772 pos += hit.getInsertionIndex();
773 }
774 }
775 }
776
777 return pos;
778 }
779
780 /**
781 * Returns the selected range info.
782 *
783 * @return Selected range info
784 */
785 protected LinePosition getSelectedRange() {
/*
P/P * Method: LinePosition getSelectedRange()
*
* Preconditions:
* this.selection != null
* init'ed(this.selection.endLine)
* init'ed(this.selection.endPos)
* init'ed(this.selection.startLine)
* init'ed(this.selection.startPos)
*
* Postconditions:
* return_value in Addr_Set{&new LinePosition(getSelectedRange#2),&new LinePosition(getSelectedRange#3),&new LinePosition(getSelectedRange#1)}
* new LinePosition(getSelectedRange#1) num objects <= 1
* new LinePosition(getSelectedRange#1).endLine == this.selection.startLine
* new LinePosition(getSelectedRange#1).endLine >= -231+1
* new LinePosition(getSelectedRange#1).endPos == this.selection.startPos
* init'ed(new LinePosition(getSelectedRange#1).endPos)
* new LinePosition(getSelectedRange#1).startLine == this.selection.endLine
* new LinePosition(getSelectedRange#1).startLine <= 232-2
* new LinePosition(getSelectedRange#1).startPos == this.selection.endPos
* init'ed(new LinePosition(getSelectedRange#1).startPos)
* ...
*
* Test Vectors:
* this.selection.endLine - this.selection.startLine: {1..6_442_450_943}, {-6_442_450_943..-1}, {0}
* this.selection.endPos - this.selection.startPos: {0..6_442_450_943}, {-6_442_450_943..-1}
*/
786 if (selection.getStartLine() > selection.getEndLine()) {
787 // Swap both
788 return new LinePosition(selection.getEndLine(),
789 selection.getEndPos(), selection.getStartLine(),
790 selection.getStartPos());
791 } else if (selection.getStartLine() == selection.getEndLine() &&
792 selection.getStartPos() > selection.getEndPos()) {
793 // Just swap the chars
794 return new LinePosition(selection.getStartLine(), selection.
795 getEndPos(), selection.getEndLine(),
796 selection.getStartPos());
797 } else {
798 // Swap nothing
799 return new LinePosition(selection.getStartLine(), selection.
800 getStartPos(), selection.getEndLine(),
801 selection.getEndPos());
802 }
803 }
804
805 /** Clears the selection. */
806 protected void clearSelection() {
/*
P/P * Method: void clearSelection()
*
* Preconditions:
* this.selection != null
* init'ed(this.selection.startLine)
* init'ed(this.selection.startPos)
*
* Postconditions:
* this.selection.endLine == this.selection.startLine
* init'ed(this.selection.endLine)
* this.selection.endPos == this.selection.startPos
* init'ed(this.selection.endPos)
*
* Test Vectors:
* com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas:isVisible(...)@809: {0}, {1}
*/
807 selection.setEndLine(selection.getStartLine());
808 selection.setEndPos(selection.getStartPos());
809 if (isVisible()) {
810 repaint();
811 }
812 }
813
814 /**
815 * Selects the specified region of text.
816 *
817 * @param position Line position
818 */
819 public void setSelectedRange(final LinePosition position) {
/*
P/P * Method: void setSelectedRange(LinePosition)
*
* Preconditions:
* position != null
* init'ed(position.endLine)
* init'ed(position.endPos)
* init'ed(position.startLine)
* init'ed(position.startPos)
*
* Postconditions:
* this.selection == &new LinePosition(setSelectedRange#1)
* new LinePosition(setSelectedRange#1) num objects == 1
* this.selection.endLine == position.endLine
* init'ed(this.selection.endLine)
* this.selection.endPos == position.endPos
* init'ed(this.selection.endPos)
* this.selection.startLine == position.startLine
* init'ed(this.selection.startLine)
* this.selection.startPos == position.startPos
* init'ed(this.selection.startPos)
*
* Test Vectors:
* com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas:isVisible(...)@821: {0}, {1}
*/
820 selection = new LinePosition(position);
821 if (isVisible()) {
822 repaint();
823 }
824 }
825
826 /**nee
827 * Returns the first visible line.
828 *
829 * @return the line number of the first visible line
830 */
831 public int getFirstVisibleLine() {
/*
P/P * Method: int getFirstVisibleLine()
*
* Preconditions:
* init'ed(this.firstVisibleLine)
*
* Postconditions:
* return_value == this.firstVisibleLine
* init'ed(return_value)
*/
832 return firstVisibleLine;
833 }
834
835 /**
836 * Returns the last visible line.
837 *
838 * @return the line number of the last visible line
839 */
840 public int getLastVisibleLine() {
/*
P/P * Method: int getLastVisibleLine()
*
* Preconditions:
* init'ed(this.lastVisibleLine)
*
* Postconditions:
* return_value == this.lastVisibleLine
* init'ed(return_value)
*/
841 return lastVisibleLine;
842 }
843
844 /**
845 * {@inheritDoc}
846 *
847 * @param e Component event
848 */
849 @Override
850 public void componentResized(final ComponentEvent e) {
851 //line wrap cache now invalid, clear and repaint
/*
P/P * Method: void componentResized(ComponentEvent)
*
* Preconditions:
* this.lineWrap != null
*
* Test Vectors:
* com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas:isVisible(...)@853: {0}, {1}
*/
852 lineWrap.clear();
853 if (isVisible()) {
854 repaint();
855 }
856 }
857
858 /**
859 * {@inheritDoc}
860 *
861 * @param e Component event
862 */
863 @Override
864 public void componentMoved(final ComponentEvent e) {
865 //Ignore
/*
P/P * Method: void componentMoved(ComponentEvent)
*/
866 }
867
868 /**
869 * {@inheritDoc}
870 *
871 * @param e Component event
872 */
873 @Override
874 public void componentShown(final ComponentEvent e) {
875 //Ignore
/*
P/P * Method: void componentShown(ComponentEvent)
*/
876 }
877
878 /**
879 * {@inheritDoc}
880 *
881 * @param e Component event
882 */
883 @Override
884 public void componentHidden(final ComponentEvent e) {
885 //Ignore
/*
P/P * Method: void componentHidden(ComponentEvent)
*/
886 }
887
888 /** Clears the line wrapping cache. */
889 protected void clearWrapCache() {
/*
P/P * Method: void clearWrapCache()
*/
890 UIUtilities.invokeLater(new Runnable() {
891
892 /** {@inheritDoc} */
893 @Override
894 public void run() {
/*
P/P * Method: void run()
*
* Preconditions:
* this.lineWrap != null
*/
895 lineWrap.clear();
896 }
897 });
898 }
899
900 /** {@inheritDoc} */
901 @Override
902 public void configChanged(final String domain, final String key) {
/*
P/P * Method: void configChanged(String, String)
*/
903 UIUtilities.invokeLater(new Runnable() {
904
905 /** {@inheritDoc} */
906 @Override
907 public void run() {
/*
P/P * Method: void run()
*
* Test Vectors:
* com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas:isVisible(...)@908: {0}, {1}
*/
908 if (isVisible()) {
909 repaint();
910 }
911 }
912 });
913 }
914 }
SofCheck Inspector Build Version : 2.17854
| TextPaneCanvas.java |
2009-Jun-25 01:54:24 |
| TextPaneCanvas.class |
2009-Sep-02 17:04:14 |
| TextPaneCanvas$1.class |
2009-Sep-02 17:04:14 |
| TextPaneCanvas$2.class |
2009-Sep-02 17:04:14 |