TextPaneCanvas.java

TextPaneCanvas.java

current inspection = 2009-09-03 21:56:13 (id #1)

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

Map access$000(TextPaneCanvas)

Kind	Annotation Text
pre	x0 != null
post	init'ed(return_value)
post	return_value == x0.lineWrap

void checkForLink()

Kind	Annotation Text
pre	(soft) this.document != null
pre	(soft) this.document.cachedLines != null
pre	(soft) this.document.cachedStrings != null
pre	(soft) this.document.lines != null
pre	(soft) this.positions != null
pre	(soft) this.textLayouts != null
presumption	init'ed(com.dmdirc.ui.messages.IRCTextAttribute. CHANNEL)
presumption	init'ed(com.dmdirc.ui.messages.IRCTextAttribute. HYPERLINK)
presumption	init'ed(com.dmdirc.ui.messages.IRCTextAttribute. NICKNAME)
presumption	java.text.AttributedCharacterIterator:getAttributes (...)@646 != null
presumption	java.text.AttributedCharacterIterator:getAttributes (...)@652 != null
presumption	java.text.AttributedCharacterIterator:getAttributes (...)@657 != null
presumption	java.text.AttributedString:getIterator(...)@253 != null
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on com.dmdirc.ui.messages.Styliser:getStyledSt ring
unanalyzed	call on com.dmdirc.util.ConfigFile:getKeyDomain
unanalyzed	call on com.dmdirc.util.ConfigFile:isKeyDomain
unanalyzed	call on com.dmdirc.util.RollingList:add
unanalyzed	call on com.dmdirc.util.RollingList:contains
unanalyzed	call on com.dmdirc.util.RollingList:get
unanalyzed	call on com.dmdirc.util.RollingList:getList
unanalyzed	call on getOption
unanalyzed	call on getStyledLine
unanalyzed	call on hasOption
unanalyzed	call on java.awt.Font
unanalyzed	call on java.awt.Font:getFamily
unanalyzed	call on java.awt.Font:getName
unanalyzed	call on java.awt.Font:getSize
unanalyzed	call on java.awt.Point:getX
unanalyzed	call on java.awt.Point:getY
unanalyzed	call on java.awt.Rectangle:contains
unanalyzed	call on java.awt.font.TextHitInfo:getInsertionIndex
unanalyzed	call on java.awt.font.TextLayout:getCharacterCount
unanalyzed	call on java.awt.font.TextLayout:hitTestChar
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on java.lang.Integer:intValue
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.text.AttributedCharacterIterator:getEn dIndex
unanalyzed	call on java.text.AttributedString
unanalyzed	call on java.text.AttributedString:addAttribute
unanalyzed	call on java.text.AttributedString:getIterator
unanalyzed	call on java.util.Enumeration:hasMoreElements
unanalyzed	call on java.util.Enumeration:nextElement
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:indexOf
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.Map$Entry:getKey
unanalyzed	call on java.util.Map$Entry:getValue
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:entrySet
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on javax.swing.UIManager:getFont
unanalyzed	call on javax.swing.text.AttributeSet:getAttribute
unanalyzed	call on javax.swing.text.AttributeSet:getAttributeN ames
unanalyzed	call on javax.swing.text.BadLocationException:getMe ssage
unanalyzed	call on javax.swing.text.Document:getLength
unanalyzed	call on javax.swing.text.Document:getText
unanalyzed	call on javax.swing.text.Element:getAttributes
unanalyzed	call on javax.swing.text.Element:getDocument
unanalyzed	call on javax.swing.text.Element:getElement
unanalyzed	call on javax.swing.text.Element:getElementCount
unanalyzed	call on javax.swing.text.Element:getEndOffset
unanalyzed	call on javax.swing.text.Element:getStartOffset
unanalyzed	call on javax.swing.text.StyledDocument:getParagrap hElement
test_vector	com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:getCursor(...)@663: Inverse{&new Cursor(TextPaneCanvas__static_init#1)}, Addr_Set{&new Cursor(TextPaneCanvas__static_in it#1)}
test_vector	java.util.List:get(...)@89: Addr_Set{null}, Inverse{null}

void clearSelection()

Kind	Annotation Text
pre	init'ed(this.selection.startLine)
pre	init'ed(this.selection.startPos)
pre	this.selection != null
post	init'ed(this.selection.endLine)
post	init'ed(this.selection.endPos)
post	this.selection.endLine == this.selection.startLine
post	this.selection.endPos == this.selection.startPos
test_vector	com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:isVisible(...)@809: {0}, {1}

void clearWrapCache()

Kind	Annotation Text

void com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas$1(TextPaneCanvas)

Kind	Annotation Text

com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas$1__static_init

Kind	Annotation Text

void com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas$2(TextPaneCanvas)

Kind	Annotation Text

com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas$2__static_init

Kind	Annotation Text

void com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas(TextPane, IRCDocument)

Kind	Annotation Text
post	init'ed(this.document)
post	init'ed(this.scrollBarPosition)
post	init'ed(this.selection.endLine)
post	init'ed(this.selection.endPos)
post	init'ed(this.selection.startLine)
post	init'ed(this.selection.startPos)
post	init'ed(this.textPane)
post	new HashMap(TextPaneCanvas#1) num objects == 1
post	new HashMap(TextPaneCanvas#2) num objects == 1
post	new HashMap(TextPaneCanvas#3) num objects == 1
post	new LinePosition(TextPaneCanvas#4) num objects == 1
post	this.document == document
post	this.lineWrap == &new HashMap(TextPaneCanvas#3)
post	this.positions == &new HashMap(TextPaneCanvas#2 )
post	this.selection == &new LinePosition(TextPaneCan vas#4)
post	this.textLayouts == &new HashMap(TextPaneCanvas #1)
post	this.textPane == parent

com.dmdirc.addons.ui_swing.textpane.TextPaneCanvas__static_init

Kind	Annotation Text
post	HAND_CURSOR == &new Cursor(TextPaneCanvas__ static_init#1)
post	new Cursor(TextPaneCanvas__static_init#1) num objects == 1

void componentHidden(ComponentEvent)

Kind	Annotation Text

void componentMoved(ComponentEvent)

Kind	Annotation Text

void componentResized(ComponentEvent)

Kind	Annotation Text
pre	this.lineWrap != null
test_vector	com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:isVisible(...)@853: {0}, {1}

void componentShown(ComponentEvent)

Kind	Annotation Text

void configChanged(String, String)

Kind	Annotation Text

void doHighlight(int, int, TextLayout, Graphics2D, float, float)

Kind	Annotation Text
pre	(soft) g != null
pre	(soft) layout != null
pre	(soft) this.document != null
pre	(soft) this.document.cachedLines != null
pre	(soft) this.document.cachedStrings != null
pre	(soft) this.document.lines != null
pre	(soft) this.textPane != null
pre	init'ed(this.selection.endLine)
pre	init'ed(this.selection.endPos)
pre	init'ed(this.selection.startLine)
pre	init'ed(this.selection.startPos)
pre	this.selection != null
presumption	(int) ((float) (getLine(...).lineHeight)*21_617_278 _211_378_381/18_014_398_509_481_984) in {-2³¹..2³²-1}
presumption	(int) ((float) (getLineHeight(...)@333)*21_617_278_ 211_378_381/18_014_398_509_481_984) in range
presumption	(int) (drawPosY + (float) ((int) ((float) (getLine(...).lineHeight)*21_617_278_211_378_381/1 8_014_398_509_481_984))/2) in {-2³¹.. 2³²-1}
presumption	(int) (drawPosY + (float) ((int) ((float) (getLineHeight(...)@333)*21_617_278_211_378_381/18 _014_398_509_481_984))/2) in range
presumption	chars + java.awt.font.TextLayout:getCharacterCount( ...)@314 in {-2³¹..2³²-1}
presumption	com.dmdirc.ui.messages.Styliser:stipControlCodes(.. .)@107 != null
presumption	getLine(...).lineParts != null
presumption	getLine(...).lineParts.length <= 2³²-1
presumption	init'ed(java.awt.font.TextAttribute.BACKGROUND)
presumption	init'ed(java.awt.font.TextAttribute.FOREGROUND)
presumption	java.awt.Shape:getBounds(...)@352 != null
presumption	java.awt.Shape:getBounds(...)@358 != null
presumption	java.awt.font.TextLayout:getLogicalHighlightShape(. ..)@346 != null
presumption	java.util.List:get(...)@89 != null
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on com.dmdirc.ui.messages.Styliser:getStyledSt ring
unanalyzed	call on com.dmdirc.ui.messages.Styliser:stipControl Codes
unanalyzed	call on com.dmdirc.util.ConfigFile:getKeyDomain
unanalyzed	call on com.dmdirc.util.ConfigFile:isKeyDomain
unanalyzed	call on com.dmdirc.util.RollingList:add
unanalyzed	call on com.dmdirc.util.RollingList:contains
unanalyzed	call on com.dmdirc.util.RollingList:get
unanalyzed	call on com.dmdirc.util.RollingList:getList
unanalyzed	call on getLineHeight
unanalyzed	call on getOption
unanalyzed	call on getStyledLine
unanalyzed	call on hasOption
unanalyzed	call on java.awt.Font
unanalyzed	call on java.awt.Font:getFamily
unanalyzed	call on java.awt.Font:getName
unanalyzed	call on java.awt.Font:getSize
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on java.lang.Integer:intValue
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.text.AttributedCharacterIterator:getEn dIndex
unanalyzed	call on java.text.AttributedString
unanalyzed	call on java.text.AttributedString:addAttribute
unanalyzed	call on java.text.AttributedString:getIterator
unanalyzed	call on java.util.Enumeration:hasMoreElements
unanalyzed	call on java.util.Enumeration:nextElement
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:indexOf
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:put
unanalyzed	call on javax.swing.UIManager:getFont
unanalyzed	call on javax.swing.text.AttributeSet:getAttribute
unanalyzed	call on javax.swing.text.AttributeSet:getAttributeN ames
unanalyzed	call on javax.swing.text.BadLocationException:getMe ssage
unanalyzed	call on javax.swing.text.Document:getLength
unanalyzed	call on javax.swing.text.Document:getText
unanalyzed	call on javax.swing.text.Element:getAttributes
unanalyzed	call on javax.swing.text.Element:getDocument
unanalyzed	call on javax.swing.text.Element:getElement
unanalyzed	call on javax.swing.text.Element:getElementCount
unanalyzed	call on javax.swing.text.Element:getEndOffset
unanalyzed	call on javax.swing.text.Element:getStartOffset
unanalyzed	call on javax.swing.text.StyledDocument:getParagrap hElement
test_vector	java.lang.String:isEmpty(...)@327: {0}, {1}
test_vector	this.selection.endLine - this.selection.startLine: {1..6_442_450_943}, {-6_442_450_943..-1}, {0}
test_vector	this.selection.endPos - this.selection.startPos: {0..6_442_450_943}, {-6_442_450_943..-1}

Object getAttributeValueAtPoint(LineInfo)

Kind	Annotation Text
pre	(soft) init'ed(lineInfo.index)
pre	(soft) this.document != null
pre	(soft) this.document.cachedLines != null
pre	(soft) this.document.cachedStrings != null
pre	(soft) this.document.lines != null
pre	init'ed(lineInfo.line)
pre	lineInfo != null
presumption	getStyledLine(...)@475 init'ed
presumption	init'ed(com.dmdirc.ui.messages.IRCTextAttribute. CHANNEL)
presumption	init'ed(com.dmdirc.ui.messages.IRCTextAttribute. HYPERLINK)
presumption	init'ed(com.dmdirc.ui.messages.IRCTextAttribute. NICKNAME)
presumption	java.text.AttributedCharacterIterator:getAttributes (...)@478 != null
presumption	java.text.AttributedCharacterIterator:getAttributes (...)@483 != null
presumption	java.text.AttributedCharacterIterator:getAttributes (...)@487 != null
presumption	java.text.AttributedString:getIterator(...)@253 != null
post	init'ed(return_value)
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on com.dmdirc.ui.messages.Styliser:getStyledSt ring
unanalyzed	call on com.dmdirc.util.ConfigFile:getKeyDomain
unanalyzed	call on com.dmdirc.util.ConfigFile:isKeyDomain
unanalyzed	call on com.dmdirc.util.RollingList:add
unanalyzed	call on com.dmdirc.util.RollingList:contains
unanalyzed	call on com.dmdirc.util.RollingList:get
unanalyzed	call on com.dmdirc.util.RollingList:getList
unanalyzed	call on getOption
unanalyzed	call on getStyledLine
unanalyzed	call on hasOption
unanalyzed	call on java.awt.Font
unanalyzed	call on java.awt.Font:getFamily
unanalyzed	call on java.awt.Font:getName
unanalyzed	call on java.awt.Font:getSize
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on java.lang.Integer:intValue
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.text.AttributedCharacterIterator:getEn dIndex
unanalyzed	call on java.text.AttributedString
unanalyzed	call on java.text.AttributedString:addAttribute
unanalyzed	call on java.text.AttributedString:getIterator
unanalyzed	call on java.util.Enumeration:hasMoreElements
unanalyzed	call on java.util.Enumeration:nextElement
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:indexOf
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:put
unanalyzed	call on javax.swing.UIManager:getFont
unanalyzed	call on javax.swing.text.AttributeSet:getAttribute
unanalyzed	call on javax.swing.text.AttributeSet:getAttributeN ames
unanalyzed	call on javax.swing.text.BadLocationException:getMe ssage
unanalyzed	call on javax.swing.text.Document:getLength
unanalyzed	call on javax.swing.text.Document:getText
unanalyzed	call on javax.swing.text.Element:getAttributes
unanalyzed	call on javax.swing.text.Element:getDocument
unanalyzed	call on javax.swing.text.Element:getElement
unanalyzed	call on javax.swing.text.Element:getElementCount
unanalyzed	call on javax.swing.text.Element:getEndOffset
unanalyzed	call on javax.swing.text.Element:getStartOffset
unanalyzed	call on javax.swing.text.StyledDocument:getParagrap hElement
test_vector	lineInfo.line: {-1}, {-2³¹..-2, 0..2³²-1}

LineInfo getClickPosition(Point)

Kind	Annotation Text
pre	(soft) this.positions != null
pre	(soft) this.textLayouts != null
presumption	(int) (java.awt.Point:getX(...)@743) in {-2³¹..2³²-1}
presumption	(int) (java.awt.Point:getY(...)@743) in {-2³¹..2³²-1}
presumption	java.util.Iterator:next(...)@736 != null
presumption	java.util.Map:entrySet(...)@736 != null
presumption	java.util.Map:get(...)@738 != null
presumption	java.util.Map:get(...)@739 != null
presumption	java.util.Map_Entry:getKey(...)@737 != null
post	init'ed(return_value.index)
post	init'ed(return_value.line)
post	init'ed(return_value.part)
post	new LineInfo(getClickPosition#1) num objects == 1
post	return_value == &new LineInfo(getClickPosition# 1)
unanalyzed	call on java.awt.font.TextHitInfo:getInsertionIndex
unanalyzed	call on java.awt.font.TextLayout:getCharacterCount
unanalyzed	call on java.awt.font.TextLayout:hitTestChar
unanalyzed	call on java.util.Map$Entry:getValue
unanalyzed	call on java.util.Map:entrySet
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Set:iterator
test_vector	java.awt.Rectangle:contains(...)@737: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@736: {0}, {1}
test_vector	point: Addr_Set{null}, Inverse{null}

ClickType getClickType(LineInfo)

Kind	Annotation Text
pre	(soft) init'ed(lineInfo.index)
pre	(soft) this.document != null
pre	(soft) this.document.cachedLines != null
pre	(soft) this.document.cachedStrings != null
pre	(soft) this.document.lines != null
pre	init'ed(lineInfo.line)
pre	lineInfo != null
presumption	getStyledLine(...)@439 init'ed
presumption	init'ed(com.dmdirc.ui.messages.IRCTextAttribute. CHANNEL)
presumption	init'ed(com.dmdirc.ui.messages.IRCTextAttribute. HYPERLINK)
presumption	init'ed(com.dmdirc.ui.messages.IRCTextAttribute. NICKNAME)
presumption	java.text.AttributedCharacterIterator:getAttributes (...)@444 != null
presumption	java.text.AttributedCharacterIterator:getAttributes (...)@449 != null
presumption	java.text.AttributedCharacterIterator:getAttributes (...)@454 != null
presumption	java.text.AttributedString:getIterator(...)@253 != null
post	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_i nit.new ClickType(ClickType__static_init#2), &com.dmdir...
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on com.dmdirc.ui.messages.Styliser:getStyledSt ring
unanalyzed	call on com.dmdirc.util.ConfigFile:getKeyDomain
unanalyzed	call on com.dmdirc.util.ConfigFile:isKeyDomain
unanalyzed	call on com.dmdirc.util.RollingList:add
unanalyzed	call on com.dmdirc.util.RollingList:contains
unanalyzed	call on com.dmdirc.util.RollingList:get
unanalyzed	call on com.dmdirc.util.RollingList:getList
unanalyzed	call on getOption
unanalyzed	call on getStyledLine
unanalyzed	call on hasOption
unanalyzed	call on java.awt.Font
unanalyzed	call on java.awt.Font:getFamily
unanalyzed	call on java.awt.Font:getName
unanalyzed	call on java.awt.Font:getSize
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on java.lang.Integer:intValue
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.text.AttributedCharacterIterator:getEn dIndex
unanalyzed	call on java.text.AttributedString
unanalyzed	call on java.text.AttributedString:addAttribute
unanalyzed	call on java.text.AttributedString:getIterator
unanalyzed	call on java.util.Enumeration:hasMoreElements
unanalyzed	call on java.util.Enumeration:nextElement
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:indexOf
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:put
unanalyzed	call on javax.swing.UIManager:getFont
unanalyzed	call on javax.swing.text.AttributeSet:getAttribute
unanalyzed	call on javax.swing.text.AttributeSet:getAttributeN ames
unanalyzed	call on javax.swing.text.BadLocationException:getMe ssage
unanalyzed	call on javax.swing.text.Document:getLength
unanalyzed	call on javax.swing.text.Document:getText
unanalyzed	call on javax.swing.text.Element:getAttributes
unanalyzed	call on javax.swing.text.Element:getDocument
unanalyzed	call on javax.swing.text.Element:getElement
unanalyzed	call on javax.swing.text.Element:getElementCount
unanalyzed	call on javax.swing.text.Element:getEndOffset
unanalyzed	call on javax.swing.text.Element:getStartOffset
unanalyzed	call on javax.swing.text.StyledDocument:getParagrap hElement
test_vector	lineInfo.line: {-1}, {-2³¹..-2, 0..2³²-1}

int getFirstVisibleLine()

Kind	Annotation Text
pre	init'ed(this.firstVisibleLine)
post	init'ed(return_value)
post	return_value == this.firstVisibleLine

int getHitPosition(int, int, int, int)

Kind	Annotation Text
pre	(soft) this.textLayouts != null
pre	this.positions != null
presumption	java.awt.font.TextLayout:hitTestChar(...)@770 != null
presumption	java.util.Iterator:next(...)@764 != null
presumption	java.util.Map:entrySet(...)@764 != null
presumption	java.util.Map:get(...)@765 != null
presumption	java.util.Map:get(...)@766 != null
presumption	java.util.Map:get(...)@768 != null
presumption	java.util.Map_Entry:getValue(...)@767 != null
presumption	java.util.Map_Entry:getValue(...)@770 != null
post	init'ed(return_value)
test_vector	java.util.Iterator:hasNext(...)@764: {0}, {1}

int getLastVisibleLine()

Kind	Annotation Text
pre	init'ed(this.lastVisibleLine)
post	init'ed(return_value)
post	return_value == this.lastVisibleLine

int getNumWrappedLines(LineBreakMeasurer, int, int, float)

Kind	Annotation Text
pre	lineMeasurer != null
post	return_value >= 0

int getScrollBarPosition()

Kind	Annotation Text
pre	init'ed(this.scrollBarPosition)
post	init'ed(return_value)
post	return_value == this.scrollBarPosition

LinePosition getSelectedRange()

Kind	Annotation Text
pre	init'ed(this.selection.endLine)
pre	init'ed(this.selection.endPos)
pre	init'ed(this.selection.startLine)
pre	init'ed(this.selection.startPos)
pre	this.selection != null
post	init'ed(new LinePosition(getSelectedRange#1). endPos)
post	init'ed(new LinePosition(getSelectedRange#1). startPos)
post	init'ed(new LinePosition(getSelectedRange#2). endLine)
post	init'ed(new LinePosition(getSelectedRange#2). startLine)
post	init'ed(new LinePosition(getSelectedRange#3). endLine)
post	init'ed(new LinePosition(getSelectedRange#3). endPos)
post	init'ed(new LinePosition(getSelectedRange#3). startLine)
post	init'ed(new LinePosition(getSelectedRange#3). startPos)
post	new LinePosition(getSelectedRange#1) num objects <= 1
post	new LinePosition(getSelectedRange#1).endLine == this.selection.startLine
post	new LinePosition(getSelectedRange#1).endLine >= -2³¹+1
post	new LinePosition(getSelectedRange#1).endPos == this.selection.startPos
post	new LinePosition(getSelectedRange#1).startLine <= 2³²-2
post	new LinePosition(getSelectedRange#1).startLine == this.selection.endLine
post	new LinePosition(getSelectedRange#1).startPos == this.selection.endPos
post	new LinePosition(getSelectedRange#2) num objects <= 1
post	new LinePosition(getSelectedRange#2).endLine == this.selection.endLine
post	new LinePosition(getSelectedRange#2).endPos == this.selection.startPos
post	new LinePosition(getSelectedRange#2).endPos >= -2³¹+1
post	new LinePosition(getSelectedRange#2).startLine == this.selection.startLine
post	new LinePosition(getSelectedRange#2).startPos <= 2³²-2
post	new LinePosition(getSelectedRange#2).startPos == this.selection.endPos
post	new LinePosition(getSelectedRange#3) num objects <= 1
post	new LinePosition(getSelectedRange#3).endLine == this.selection.endLine
post	new LinePosition(getSelectedRange#3).endPos == this.selection.endPos
post	new LinePosition(getSelectedRange#3).startLine == this.selection.startLine
post	new LinePosition(getSelectedRange#3).startPos == this.selection.startPos
post	return_value in Addr_Set{&new LinePosition(getS electedRange#2),&new LinePosition(getSelectedRa nge#3),&new LinePosition(getSelectedRange#1)}
test_vector	this.selection.endLine - this.selection.startLine: {1..6_442_450_943}, {-6_442_450_943..-1}, {0}
test_vector	this.selection.endPos - this.selection.startPos: {0..6_442_450_943}, {-6_442_450_943..-1}

int getSurroundingWordEnd(String, int)

Kind	Annotation Text
pre	text != null
post	init'ed(return_value)
post	return_value - index in {0..6_442_450_943}
test_vector	java.lang.String:charAt(...)@553: {32}, {0..31, 33..2¹⁶-1}

int[] getSurroundingWordIndexes(String, int)

Kind	Annotation Text
pre	text != null
post	new int[](getSurroundingWordIndexes#1) num objects <= 1
post	new int[](getSurroundingWordIndexes#1).length == 2
post	new int[](getSurroundingWordIndexes#1)[0] == 0
post	new int[](getSurroundingWordIndexes#1)[1] == 0
post	new int[](getSurroundingWordIndexes#2) num objects <= 1
post	new int[](getSurroundingWordIndexes#2).length == 2
post	new int[](getSurroundingWordIndexes#2)[0] >= 0
post	new int[](getSurroundingWordIndexes#2)[1] >= 0
post	return_value in Addr_Set{&new int[](getSurround ingWordIndexes#2),&new int[](getSurroundingWord Indexes#1)}
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:length

int getSurroundingWordStart(String, int)

Kind	Annotation Text
pre	text != null
post	init'ed(return_value)
test_vector	java.lang.String:charAt(...)@530: {32}, {0..31, 33..2¹⁶-1}
test_vector	java.lang.String:charAt(...)@533: {0..31, 33..2¹⁶-1}, {32}

void highlightEvent(MouseEventType, MouseEvent)

Kind	Annotation Text
pre	(soft) e != null
pre	(soft) this.positions != null
pre	(soft) this.selection != null
pre	(soft) this.textLayouts != null
presumption	com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:getBounds(...)@680 != null
presumption	java.awt.event.MouseEvent:getLocationOnScreen(... )@677 != null
presumption	java.awt.event.MouseEvent:getPoint(...)@681 != null
post	possibly_updated(this.selection.endLine)
post	possibly_updated(this.selection.endPos)
post	possibly_updated(this.selection.startLine)
post	possibly_updated(this.selection.startPos)
unanalyzed	call on java.awt.Point:getX
unanalyzed	call on java.awt.Point:getY
unanalyzed	call on java.awt.Rectangle:contains
unanalyzed	call on java.awt.font.TextHitInfo:getInsertionIndex
unanalyzed	call on java.awt.font.TextLayout:getCharacterCount
unanalyzed	call on java.awt.font.TextLayout:hitTestChar
unanalyzed	call on java.util.Map$Entry:getKey
unanalyzed	call on java.util.Map$Entry:getValue
unanalyzed	call on java.util.Map:entrySet
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Set:iterator
test_vector	com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:contains(...)@679: {1}, {0}
test_vector	com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:contains(...)@701: {0}, {1}
test_vector	com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:isVisible(...)@676: {0}, {1}

void mouseClicked(MouseEvent)

Kind	Annotation Text
pre	(soft) this.document != null
pre	(soft) this.document.lines != null
pre	(soft) this.positions != null
pre	(soft) this.selection != null
pre	(soft) this.textLayouts != null
pre	e != null
pre	this.textPane != null
presumption	com.dmdirc.ui.messages.Styliser:stipControlCodes(.. .)@107 != null
presumption	extent.length@406 >= 2
presumption	getLine(...).lineParts != null
presumption	getLine(...).lineParts.length <= 2³²-1
presumption	getLine(...)@400 init'ed
presumption	java.util.List:get(...)@89 != null
post	possibly_updated(this.selection.endLine)
post	possibly_updated(this.selection.endPos)
post	possibly_updated(this.selection.startLine)
post	possibly_updated(this.selection.startPos)
unanalyzed	call on com.dmdirc.ui.messages.Styliser:stipControl Codes
unanalyzed	call on java.awt.Point:getX
unanalyzed	call on java.awt.Point:getY
unanalyzed	call on java.awt.Rectangle:contains
unanalyzed	call on java.awt.font.TextHitInfo:getInsertionIndex
unanalyzed	call on java.awt.font.TextLayout:getCharacterCount
unanalyzed	call on java.awt.font.TextLayout:hitTestChar
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.Map$Entry:getKey
unanalyzed	call on java.util.Map$Entry:getValue
unanalyzed	call on java.util.Map:entrySet
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Set:iterator
test_vector	java.awt.event.MouseEvent:getClickCount(...)@413: {-2³¹..1, 3..2³²-1}, {2}
test_vector	java.awt.event.MouseEvent:getClickCount(...)@418: {-2³¹..2, 4..2³²-1}, {3}

void mouseDragged(MouseEvent)

Kind	Annotation Text
pre	(soft) this.positions != null
pre	(soft) this.selection != null
pre	(soft) this.textLayouts != null
pre	e != null
pre	this.textPane != null
post	possibly_updated(this.selection.endLine)
post	possibly_updated(this.selection.endPos)
post	possibly_updated(this.selection.startLine)
post	possibly_updated(this.selection.startPos)
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:contains
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:getBounds
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:isVisible
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:repaint
unanalyzed	call on java.awt.Point:getX
unanalyzed	call on java.awt.Point:getY
unanalyzed	call on java.awt.Point:setLocation
unanalyzed	call on java.awt.Rectangle:contains
unanalyzed	call on java.awt.Rectangle:getHeight
unanalyzed	call on java.awt.Rectangle:getWidth
unanalyzed	call on java.awt.Rectangle:getX
unanalyzed	call on java.awt.Rectangle:getY
unanalyzed	call on java.awt.event.MouseEvent:getLocationOnScre en
unanalyzed	call on java.awt.event.MouseEvent:getPoint
unanalyzed	call on java.awt.font.TextHitInfo:getInsertionIndex
unanalyzed	call on java.awt.font.TextLayout:getCharacterCount
unanalyzed	call on java.awt.font.TextLayout:hitTestChar
unanalyzed	call on java.util.Map$Entry:getKey
unanalyzed	call on java.util.Map$Entry:getValue
unanalyzed	call on java.util.Map:entrySet
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on javax.swing.SwingUtilities:convertPointFrom Screen
test_vector	java.awt.event.MouseEvent:getModifiersEx(...)@595: {-2³¹..1_023, 1_025..2³²-1}, {1_024}

void mouseEntered(MouseEvent)

Kind	Annotation Text

void mouseExited(MouseEvent)

Kind	Annotation Text

void mouseMoved(MouseEvent)

Kind	Annotation Text
pre	(soft) this.document != null
pre	(soft) this.document.cachedLines != null
pre	(soft) this.document.cachedStrings != null
pre	(soft) this.document.lines != null
pre	(soft) this.positions != null
pre	(soft) this.textLayouts != null
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:getCursor
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:getMousePosition
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:setCursor
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on com.dmdirc.ui.messages.Styliser:getStyledSt ring
unanalyzed	call on com.dmdirc.util.ConfigFile:getKeyDomain
unanalyzed	call on com.dmdirc.util.ConfigFile:isKeyDomain
unanalyzed	call on com.dmdirc.util.RollingList:add
unanalyzed	call on com.dmdirc.util.RollingList:contains
unanalyzed	call on com.dmdirc.util.RollingList:get
unanalyzed	call on com.dmdirc.util.RollingList:getList
unanalyzed	call on getLine
unanalyzed	call on getOption
unanalyzed	call on getStyledLine
unanalyzed	call on hasOption
unanalyzed	call on java.awt.Cursor:getDefaultCursor
unanalyzed	call on java.awt.Font
unanalyzed	call on java.awt.Font:getFamily
unanalyzed	call on java.awt.Font:getName
unanalyzed	call on java.awt.Font:getSize
unanalyzed	call on java.awt.Point:getX
unanalyzed	call on java.awt.Point:getY
unanalyzed	call on java.awt.Rectangle:contains
unanalyzed	call on java.awt.font.TextHitInfo:getInsertionIndex
unanalyzed	call on java.awt.font.TextLayout:getCharacterCount
unanalyzed	call on java.awt.font.TextLayout:hitTestChar
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on java.lang.Integer:intValue
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.String:instanceof
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.text.AttributedCharacterIterator:getAt tributes
unanalyzed	call on java.text.AttributedCharacterIterator:getBe ginIndex
unanalyzed	call on java.text.AttributedCharacterIterator:getEn dIndex
unanalyzed	call on java.text.AttributedCharacterIterator:setIn dex
unanalyzed	call on java.text.AttributedString
unanalyzed	call on java.text.AttributedString:addAttribute
unanalyzed	call on java.text.AttributedString:getIterator
unanalyzed	call on java.util.Enumeration:hasMoreElements
unanalyzed	call on java.util.Enumeration:nextElement
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:indexOf
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.Map$Entry:getKey
unanalyzed	call on java.util.Map$Entry:getValue
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:entrySet
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on javax.swing.UIManager:getFont
unanalyzed	call on javax.swing.text.AttributeSet:getAttribute
unanalyzed	call on javax.swing.text.AttributeSet:getAttributeN ames
unanalyzed	call on javax.swing.text.BadLocationException:getMe ssage
unanalyzed	call on javax.swing.text.Document:getLength
unanalyzed	call on javax.swing.text.Document:getText
unanalyzed	call on javax.swing.text.Element:getAttributes
unanalyzed	call on javax.swing.text.Element:getDocument
unanalyzed	call on javax.swing.text.Element:getElement
unanalyzed	call on javax.swing.text.Element:getElementCount
unanalyzed	call on javax.swing.text.Element:getEndOffset
unanalyzed	call on javax.swing.text.Element:getStartOffset
unanalyzed	call on javax.swing.text.StyledDocument:getParagrap hElement

void mousePressed(MouseEvent)

Kind	Annotation Text
pre	(soft) this.positions != null
pre	(soft) this.selection != null
pre	(soft) this.textLayouts != null
pre	e != null
pre	this.textPane != null
post	possibly_updated(this.selection.endLine)
post	possibly_updated(this.selection.endPos)
post	possibly_updated(this.selection.startLine)
post	possibly_updated(this.selection.startPos)
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:contains
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:getBounds
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:isVisible
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:repaint
unanalyzed	call on java.awt.Point:getX
unanalyzed	call on java.awt.Point:getY
unanalyzed	call on java.awt.Point:setLocation
unanalyzed	call on java.awt.Rectangle:contains
unanalyzed	call on java.awt.Rectangle:getHeight
unanalyzed	call on java.awt.Rectangle:getWidth
unanalyzed	call on java.awt.Rectangle:getX
unanalyzed	call on java.awt.Rectangle:getY
unanalyzed	call on java.awt.event.MouseEvent:getLocationOnScre en
unanalyzed	call on java.awt.event.MouseEvent:getPoint
unanalyzed	call on java.awt.font.TextHitInfo:getInsertionIndex
unanalyzed	call on java.awt.font.TextLayout:getCharacterCount
unanalyzed	call on java.awt.font.TextLayout:hitTestChar
unanalyzed	call on java.util.Map$Entry:getKey
unanalyzed	call on java.util.Map$Entry:getValue
unanalyzed	call on java.util.Map:entrySet
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on javax.swing.SwingUtilities:convertPointFrom Screen
test_vector	java.awt.event.MouseEvent:getButton(...)@567: {-2³¹..0, 2..2³²-1}, {1}

void mouseReleased(MouseEvent)

Kind	Annotation Text
pre	(soft) this.positions != null
pre	(soft) this.selection != null
pre	(soft) this.textLayouts != null
pre	e != null
pre	this.textPane != null
post	possibly_updated(this.selection.endLine)
post	possibly_updated(this.selection.endPos)
post	possibly_updated(this.selection.startLine)
post	possibly_updated(this.selection.startPos)
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:contains
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:getBounds
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:isVisible
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:repaint
unanalyzed	call on java.awt.Point:getX
unanalyzed	call on java.awt.Point:getY
unanalyzed	call on java.awt.Point:setLocation
unanalyzed	call on java.awt.Rectangle:contains
unanalyzed	call on java.awt.Rectangle:getHeight
unanalyzed	call on java.awt.Rectangle:getWidth
unanalyzed	call on java.awt.Rectangle:getX
unanalyzed	call on java.awt.Rectangle:getY
unanalyzed	call on java.awt.event.MouseEvent:getLocationOnScre en
unanalyzed	call on java.awt.event.MouseEvent:getPoint
unanalyzed	call on java.awt.font.TextHitInfo:getInsertionIndex
unanalyzed	call on java.awt.font.TextLayout:getCharacterCount
unanalyzed	call on java.awt.font.TextLayout:hitTestChar
unanalyzed	call on java.util.Map$Entry:getKey
unanalyzed	call on java.util.Map$Entry:getValue
unanalyzed	call on java.util.Map:entrySet
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on javax.swing.SwingUtilities:convertPointFrom Screen
test_vector	java.awt.event.MouseEvent:getButton(...)@581: {-2³¹..0, 2..2³²-1}, {1}

void paintComponent(Graphics)

Kind	Annotation Text
pre	(soft) init'ed(this.selection.endLine)
pre	(soft) init'ed(this.selection.endPos)
pre	(soft) init'ed(this.selection.startLine)
pre	(soft) init'ed(this.selection.startPos)
pre	(soft) this.document.cachedLines != null
pre	(soft) this.document.cachedStrings != null
pre	(soft) this.lineWrap != null
pre	(soft) this.selection != null
pre	graphics != null
pre	init'ed(this.scrollBarPosition)
pre	this.document != null
pre	this.document.lines != null
pre	this.positions != null
pre	this.textLayouts != null
pre	this.textPane != null
presumption	(int) ((float) (com.dmdirc.addons.ui_swing. textpane.TextPaneCanvas:getWidth(...)@122 - 6)) in {-2_147_483_654..4_294_967_289}
presumption	(int) ((float) (getLine(...).lineHeight)*21_617_278 _211_378_381/18_014_398_509_481_984) in {-2³¹..2³²-1}
presumption	java.awt.Toolkit:getDefaultToolkit(...)@116 != null
presumption	java.awt.font.LineBreakMeasurer:nextLayout(... )@191 != null
presumption	java.text.AttributedString:getIterator(...)@253 != null
presumption	java.util.List:size(...)@78 >= -2³¹+1
presumption	java.util.Map:get(...)@174 != null
post	possibly_updated(this.firstVisibleLine)
post	possibly_updated(this.lastVisibleLine)
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPane:getBackground
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPane:getForeground
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:getCursor
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:getMousePosition
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:setCursor
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on com.dmdirc.ui.messages.Styliser:getStyledSt ring
unanalyzed	call on com.dmdirc.ui.messages.Styliser:stipControl Codes
unanalyzed	call on com.dmdirc.util.ConfigFile:getKeyDomain
unanalyzed	call on com.dmdirc.util.ConfigFile:isKeyDomain
unanalyzed	call on com.dmdirc.util.RollingList:add
unanalyzed	call on com.dmdirc.util.RollingList:contains
unanalyzed	call on com.dmdirc.util.RollingList:get
unanalyzed	call on com.dmdirc.util.RollingList:getList
unanalyzed	call on getLine
unanalyzed	call on getLineHeight
unanalyzed	call on getOption
unanalyzed	call on getStyledLine
unanalyzed	call on hasOption
unanalyzed	call on java.awt.Cursor:getDefaultCursor
unanalyzed	call on java.awt.Font
unanalyzed	call on java.awt.Font:getFamily
unanalyzed	call on java.awt.Font:getName
unanalyzed	call on java.awt.Font:getSize
unanalyzed	call on java.awt.Graphics2D:getFontRenderContext
unanalyzed	call on java.awt.Graphics2D:translate
unanalyzed	call on java.awt.Point:getX
unanalyzed	call on java.awt.Point:getY
unanalyzed	call on java.awt.Rectangle:contains
unanalyzed	call on java.awt.Rectangle:getX
unanalyzed	call on java.awt.Shape:getBounds
unanalyzed	call on java.awt.font.LineBreakMeasurer:getPosition
unanalyzed	call on java.awt.font.LineBreakMeasurer:nextLayout
unanalyzed	call on java.awt.font.LineBreakMeasurer:setPosition
unanalyzed	call on java.awt.font.TextHitInfo:getInsertionIndex
unanalyzed	call on java.awt.font.TextLayout
unanalyzed	call on java.awt.font.TextLayout:draw
unanalyzed	call on java.awt.font.TextLayout:getCharacterCount
unanalyzed	call on java.awt.font.TextLayout:getLogicalHighligh tShape
unanalyzed	call on java.awt.font.TextLayout:hitTestChar
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on java.lang.Integer:intValue
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.String:instanceof
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.text.AttributedCharacterIterator:getAt tributes
unanalyzed	call on java.text.AttributedCharacterIterator:getBe ginIndex
unanalyzed	call on java.text.AttributedCharacterIterator:getEn dIndex
unanalyzed	call on java.text.AttributedCharacterIterator:setIn dex
unanalyzed	call on java.text.AttributedString
unanalyzed	call on java.text.AttributedString:addAttribute
unanalyzed	call on java.text.AttributedString:getIterator
unanalyzed	call on java.util.Enumeration:hasMoreElements
unanalyzed	call on java.util.Enumeration:nextElement
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:indexOf
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.Map$Entry:getKey
unanalyzed	call on java.util.Map$Entry:getValue
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:entrySet
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on javax.swing.UIManager:getFont
unanalyzed	call on javax.swing.text.AttributeSet:getAttribute
unanalyzed	call on javax.swing.text.AttributeSet:getAttributeN ames
unanalyzed	call on javax.swing.text.BadLocationException:getMe ssage
unanalyzed	call on javax.swing.text.Document:getLength
unanalyzed	call on javax.swing.text.Document:getText
unanalyzed	call on javax.swing.text.Element:getAttributes
unanalyzed	call on javax.swing.text.Element:getDocument
unanalyzed	call on javax.swing.text.Element:getElement
unanalyzed	call on javax.swing.text.Element:getElementCount
unanalyzed	call on javax.swing.text.Element:getEndOffset
unanalyzed	call on javax.swing.text.Element:getStartOffset
unanalyzed	call on javax.swing.text.StyledDocument:getParagrap hElement
test_vector	java.awt.Toolkit:getDesktopProperty(...)@116: Addr_Set{null}, Inverse{null}
test_vector	java.awt.font.TextLayout:isLeftToRight(...)@201: {0}, {1}
test_vector	java.util.List:size(...)@78: {0}, {-2³¹.. -1, 1..2³²-1}
test_vector	java.util.Map:containsKey(...)@172: {0}, {1}

void run()

Kind	Annotation Text
pre	this.lineWrap != null

void run()

Kind	Annotation Text
test_vector	com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:isVisible(...)@908: {0}, {1}

void setScrollBarPosition(int)

Kind	Annotation Text
pre	(soft) this.textPane != null
pre	init'ed(this.scrollBarPosition)
post	init'ed(this.scrollBarPosition)
post	this.scrollBarPosition == One-of{old this.scrollBarPosition, position}
test_vector	com.dmdirc.addons.ui_swing.textpane. TextPane:isVisible(...)@371: {0}, {1}
test_vector	this.scrollBarPosition - position: {0}, {-6_442_450_943..-1, 1..6_442_450_943}

void setSelectedRange(LinePosition)

Kind	Annotation Text
pre	init'ed(position.endLine)
pre	init'ed(position.endPos)
pre	init'ed(position.startLine)
pre	init'ed(position.startPos)
pre	position != null
post	init'ed(this.selection.endLine)
post	init'ed(this.selection.endPos)
post	init'ed(this.selection.startLine)
post	init'ed(this.selection.startPos)
post	new LinePosition(setSelectedRange#1) num objects == 1
post	this.selection == &new LinePosition(setSelected Range#1)
post	this.selection.endLine == position.endLine
post	this.selection.endPos == position.endPos
post	this.selection.startLine == position.startLine
post	this.selection.startPos == position.startPos
test_vector	com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:isVisible(...)@821: {0}, {1}