TextPane.java

TextPane.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

JScrollBar access$000(TextPane)

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

TextPaneCanvas access$100(TextPane)

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

void adjustmentValueChanged(AdjustmentEvent)

Kind	Annotation Text
pre	(soft) this.canvas.textPane != null
pre	e != null
pre	init'ed(this.canvas.scrollBarPosition)
pre	this.canvas != null
pre	this.scrollBar != null
post	init'ed(this.canvas.scrollBarPosition)
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPane:isVisible
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:repaint
unanalyzed	call on javax.swing.JScrollBar:setValue

void clear()

Kind	Annotation Text
pre	(soft) this.canvas.textPane != null
pre	init'ed(this.canvas.scrollBarPosition)
pre	this.canvas != null
pre	this.document != null
pre	this.document.lines != null
pre	this.document.listeners != null
pre	this.scrollBar != null
post	init'ed(this.canvas.scrollBarPosition)
unanalyzed	call on cleared
unanalyzed	call on com.dmdirc.addons.ui_swing.UIUtilities:invo keLater
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPane:isVisible
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:repaint
unanalyzed	call on fireCleared
unanalyzed	call on getNumLines
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.List:clear
unanalyzed	call on java.util.List:size
unanalyzed	call on javax.swing.JScrollBar:getValue
unanalyzed	call on javax.swing.JScrollBar:getValueIsAdjusting
unanalyzed	call on javax.swing.JScrollBar:setMaximum
unanalyzed	call on javax.swing.JScrollBar:setValue
unanalyzed	call on javax.swing.event.EventListenerList:getList enerList

void clearSelection()

Kind	Annotation Text
pre	init'ed(this.canvas.selection.startLine)
pre	init'ed(this.canvas.selection.startPos)
pre	this.canvas != null
pre	this.canvas.selection != null
post	init'ed(this.canvas.selection.endLine)
post	init'ed(this.canvas.selection.endPos)
post	this.canvas.selection.endLine == this.canvas. selection.startLine
post	this.canvas.selection.endPos == this.canvas. selection.startPos
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:isVisible
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:repaint

void cleared()

Kind	Annotation Text
pre	this.canvas != null
unanalyzed	call on com.dmdirc.addons.ui_swing.UIUtilities:invo keLater

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

Kind	Annotation Text

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

Kind	Annotation Text

void com.dmdirc.addons.ui_swing.textpane.TextPane(FrameContainer)

Kind	Annotation Text
pre	frame != null
presumption	com.dmdirc.FrameContainer:getConfigManager(...). listeners@75 != null
presumption	com.dmdirc.FrameContainer:getConfigManager(...)@75 != null
post	init'ed(new LinePosition(TextPaneCanvas#4). endLine)
post	init'ed(new LinePosition(TextPaneCanvas#4).endPos)
post	init'ed(new LinePosition(TextPaneCanvas#4). startLine)
post	init'ed(new LinePosition(TextPaneCanvas#4). startPos)
post	init'ed(this.canvas.scrollBarPosition)
post	init'ed(this.document.config)
post	new ArrayList(IRCDocument#1) num objects == 1
post	new EventListenerList(IRCDocument#2) num objects == 1
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 IRCDocument(TextPane#2) num objects == 1
post	new JScrollBar(TextPane#5) num objects == 1
post	new LinePosition(TextPaneCanvas#4) num objects == 1
post	new RollingList(IRCDocument#3) num objects == 1
post	new RollingList(IRCDocument#4) num objects == 1
post	new TextPaneCanvas(TextPane#4) num objects == 1
post	this.canvas == &new TextPaneCanvas(TextPane#4)
post	this.canvas.document == &new IRCDocument(TextPa ne#2)
post	this.canvas.lineWrap == &new HashMap(TextPaneCa nvas#3)
post	this.canvas.positions == &new HashMap(TextPaneC anvas#2)
post	this.canvas.selection == &new LinePosition(Text PaneCanvas#4)
post	this.canvas.textLayouts == &new HashMap(TextPaneCanvas#1)
post	this.canvas.textPane != null
post	this.canvas.textPane == this
post	this.document == &new IRCDocument(TextPane#2)
post	this.document.cachedLines == &new RollingList(IRCDocument#3)
post	this.document.cachedStrings == &new RollingList(IRCDocument#4)
post	this.document.lines == &new ArrayList(IRCDocume nt#1)
post	this.document.listeners == &new EventListenerList(IRCDocument#2)
post	this.frame != null
post	this.frame == frame
post	this.scrollBar == &new JScrollBar(TextPane#5)
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:addComponentListener
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:addMouseListener
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:addMouseMotionListener
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:setDoubleBuffered
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:setOpaque
unanalyzed	call on com.dmdirc.util.MapList:add
unanalyzed	call on com.dmdirc.util.RollingList
unanalyzed	call on java.awt.event.MouseMotionAdapter
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.List:size
unanalyzed	call on javax.swing.JPanel
unanalyzed	call on javax.swing.event.EventListenerList
unanalyzed	call on javax.swing.event.EventListenerList:add
unanalyzed	call on javax.swing.plaf.ComponentUI

com.dmdirc.addons.ui_swing.textpane.TextPane__static_init

Kind	Annotation Text

void copy()

Kind	Annotation Text
pre	(soft) this.document != null
pre	(soft) this.document.lines != null
pre	init'ed(this.canvas.selection.endLine)
pre	init'ed(this.canvas.selection.endPos)
pre	init'ed(this.canvas.selection.startLine)
pre	init'ed(this.canvas.selection.startPos)
pre	this.canvas != null
pre	this.canvas.selection != null
presumption	java.awt.Toolkit:getDefaultToolkit(...)@340 != null
presumption	java.awt.Toolkit:getSystemClipboard(...)@340 != null
unanalyzed	call on com.dmdirc.ui.messages.Styliser:stipControl Codes
unanalyzed	call on getLine
unanalyzed	call on getNumLines
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.util.List:get
unanalyzed	call on java.util.List:size
test_vector	java.lang.String:isEmpty(...)@339: {1}, {0}

Object getAttributeValueAtPoint(LineInfo)

Kind	Annotation Text
pre	(soft) init'ed(lineInfo.index)
pre	(soft) this.canvas.document != null
pre	(soft) this.canvas.document.cachedLines != null
pre	(soft) this.canvas.document.cachedStrings != null
pre	(soft) this.canvas.document.lines != null
pre	init'ed(lineInfo.line)
pre	lineInfo != null
pre	this.canvas != 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: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: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: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

LineInfo getClickPosition(Point)

Kind	Annotation Text
pre	(soft) this.canvas.positions != null
pre	(soft) this.canvas.textLayouts != null
pre	this.canvas != null
post	init'ed(new LineInfo(getClickPosition#1*).index)
post	init'ed(new LineInfo(getClickPosition#1*).line)
post	init'ed(new LineInfo(getClickPosition#1*).part)
post	new LineInfo(getClickPosition#1*) num objects == 1
post	return_value == &new LineInfo(getClickPosition# 1*)
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

ClickType getClickType(LineInfo)

Kind	Annotation Text
pre	(soft) init'ed(lineInfo.index)
pre	(soft) this.canvas.document != null
pre	(soft) this.canvas.document.cachedLines != null
pre	(soft) this.canvas.document.cachedStrings != null
pre	(soft) this.canvas.document.lines != null
pre	init'ed(lineInfo.line)
pre	lineInfo != null
pre	this.canvas != null
post	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__sta tic_init#2), &com.dmdir...
post	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_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: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: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

IRCDocument getDocument()

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

FrameContainer getFrameContainer()

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

int getLastVisibleLine()

Kind	Annotation Text
pre	this.scrollBar != null
post	init'ed(return_value)

LinePosition getSelectedRange()

Kind	Annotation Text
pre	init'ed(this.canvas.selection.endLine)
pre	init'ed(this.canvas.selection.endPos)
pre	init'ed(this.canvas.selection.startLine)
pre	init'ed(this.canvas.selection.startPos)
pre	this.canvas != null
pre	this.canvas.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.canvas.selection.startLine
post	new LinePosition(getSelectedRange#1*).endLine >= -2³¹+1
post	new LinePosition(getSelectedRange#1*).endPos == this.canvas.selection.startPos
post	new LinePosition(getSelectedRange#1*).startLine <= 2³²-2
post	new LinePosition(getSelectedRange#1*).startLine == this.canvas.selection.endLine
post	new LinePosition(getSelectedRange#1*).startPos == this.canvas.selection.endPos
post	new LinePosition(getSelectedRange#2*) num objects <= 1
post	new LinePosition(getSelectedRange#2*).endLine == this.canvas.selection.endLine
post	new LinePosition(getSelectedRange#2*).endPos == this.canvas.selection.startPos
post	new LinePosition(getSelectedRange#2*).endPos >= -2³¹+1
post	new LinePosition(getSelectedRange#2*).startLine == this.canvas.selection.startLine
post	new LinePosition(getSelectedRange#2*).startPos <= 2³²-2
post	new LinePosition(getSelectedRange#2*).startPos == this.canvas.selection.endPos
post	new LinePosition(getSelectedRange#3*) num objects <= 1
post	new LinePosition(getSelectedRange#3*).endLine == this.canvas.selection.endLine
post	new LinePosition(getSelectedRange#3*).endPos == this.canvas.selection.endPos
post	new LinePosition(getSelectedRange#3*).startLine == this.canvas.selection.startLine
post	new LinePosition(getSelectedRange#3*).startPos == this.canvas.selection.startPos
post	return_value == One-of{&new LinePosition(getSel ectedRange#1), &new LinePosition(getSelectedRa nge#2), &new LinePosition(getSelectedRange#3*) }
post	return_value in Addr_Set{&new LinePosition(getS electedRange#1),&new LinePosition(getSelectedR ange#2),&new LinePosition(getSelectedRange#3*) }

String getSelectedText()

Kind	Annotation Text
pre	(soft) this.document != null
pre	(soft) this.document.lines != null
pre	init'ed(this.canvas.selection.endLine)
pre	init'ed(this.canvas.selection.endPos)
pre	init'ed(this.canvas.selection.startLine)
pre	init'ed(this.canvas.selection.startPos)
pre	this.canvas != null
pre	this.canvas.selection != null
presumption	com.dmdirc.ui.messages.Styliser:stipControlCodes(.. .)@107 != null
presumption	getLine(...).lineParts != null
presumption	getLine(...).lineParts.length <= 2³²-1
presumption	java.util.List:get(...)@89 != null
post	java.lang.StringBuffer:toString(...)._tainted == 0
post	return_value in Addr_Set{null,&java.lang. StringBuffer:toString(...),&java.lang. StringBuffer:toString(...)}
unanalyzed	call on com.dmdirc.ui.messages.Styliser:stipControl Codes
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:size
test_vector	java.lang.String:isEmpty(...)@235: {1}, {0}

String getWordAtIndex(int, int)

Kind	Annotation Text
pre	(soft) this.canvas != null
pre	(soft) this.document != null
pre	(soft) this.document.lines != null
presumption	com.dmdirc.ui.messages.Styliser:stipControlCodes(.. .)@107 != null
presumption	getLine(...).lineParts != null
presumption	getLine(...).lineParts.length <= 2³²-1
presumption	getLine(...)@318 init'ed
presumption	indexes.length@318 >= 2
presumption	java.util.List:get(...)@89 != null
post	java.lang.String:substring(...)._tainted == 0
post	return_value in Addr_Set{&java.lang. String:substring(...),&""}
unanalyzed	call on com.dmdirc.ui.messages.Styliser:stipControl Codes
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.util.List:get
test_vector	lineNumber: {-2³¹..-2, 0..2³²-1}, {-1}

bool hasSelectedRange()

Kind	Annotation Text
pre	init'ed(this.canvas.selection.endLine)
pre	init'ed(this.canvas.selection.endPos)
pre	init'ed(this.canvas.selection.startLine)
pre	init'ed(this.canvas.selection.startPos)
pre	this.canvas != null
pre	this.canvas.selection != null
post	init'ed(return_value)

void lineAdded(int, int)

Kind	Annotation Text
pre	(soft) init'ed(this.canvas.scrollBarPosition)
pre	(soft) this.canvas != null
pre	(soft) this.canvas.textPane != null
pre	this.document != null
pre	this.document.lines != null
pre	this.scrollBar != null
post	init'ed(this.canvas.scrollBarPosition)
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPane:isVisible
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:repaint
unanalyzed	call on getNumLines
unanalyzed	call on java.util.List:size
unanalyzed	call on javax.swing.JScrollBar:getValue
unanalyzed	call on javax.swing.JScrollBar:getValueIsAdjusting
unanalyzed	call on javax.swing.JScrollBar:setMaximum
unanalyzed	call on javax.swing.JScrollBar:setValue

void linesAdded(int, int, int)

Kind	Annotation Text
pre	(soft) init'ed(this.canvas.scrollBarPosition)
pre	(soft) this.canvas != null
pre	(soft) this.canvas.textPane != null
pre	this.document != null
pre	this.document.lines != null
pre	this.scrollBar != null
post	init'ed(this.canvas.scrollBarPosition)
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPane:isVisible
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:repaint
unanalyzed	call on getNumLines
unanalyzed	call on java.util.List:size
unanalyzed	call on javax.swing.JScrollBar:getValue
unanalyzed	call on javax.swing.JScrollBar:getValueIsAdjusting
unanalyzed	call on javax.swing.JScrollBar:setMaximum
unanalyzed	call on javax.swing.JScrollBar:setValue

void mouseDragged(MouseEvent)

Kind	Annotation Text
pre	(soft) init'ed(this.canvas.scrollBarPosition)
pre	(soft) this.canvas != null
pre	(soft) this.canvas.positions != null
pre	(soft) this.canvas.selection != null
pre	(soft) this.canvas.textLayouts != null
pre	(soft) this.canvas.textPane != null
pre	(soft) this.scrollBar != null
pre	e != null
presumption	com.dmdirc.addons.ui_swing.textpane. TextPane:getLocationOnScreen(...)@102 != null
presumption	com.dmdirc.addons.ui_swing.textpane. TextPane:getLocationOnScreen(...)@104 != null
presumption	com.dmdirc.addons.ui_swing.textpane. TextPane:getLocationOnScreen(...)@98 != null
presumption	javax.swing.JScrollBar:getValue(...)@103 >= -2³¹+1
presumption	javax.swing.JScrollBar:getValue(...)@106 <= 2³²-2
post	init'ed(this.canvas.scrollBarPosition)
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPane:isVisible
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.JScrollBar:setValue
unanalyzed	call on javax.swing.SwingUtilities:convertPointFrom Screen
test_vector	java.awt.event.MouseEvent:getModifiersEx(...)@98: {-2³¹..1_023, 1_025..2³²-1}, {1_024}

void mouseWheelMoved(MouseWheelEvent)

Kind	Annotation Text
pre	(soft) e != null
pre	(soft) init'ed(this.canvas.scrollBarPosition)
pre	(soft) this.canvas != null
pre	(soft) this.canvas.textPane != null
pre	this.scrollBar != null
presumption	java.awt.event.MouseWheelEvent:getScrollAmount(... )@190 - javax.swing.JScrollBar:getValue(...)@190 in {-2³²+1..2³¹}
presumption	javax.swing.JScrollBar:getValue(...)@188 + java.awt.event.MouseWheelEvent:getScrollAmount(... )@188 in {-2³¹..2³²-1}
post	init'ed(this.canvas.scrollBarPosition)
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPane:isVisible
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:repaint
unanalyzed	call on javax.swing.JScrollBar:setValue
test_vector	java.awt.event.MouseWheelEvent:getWheelRotation(... )@187: {-2³¹..0}, {1..2³²-1}
test_vector	javax.swing.JScrollBar:isEnabled(...)@186: {0}, {1}

void pageDown()

Kind	Annotation Text
pre	(soft) this.canvas.textPane != null
pre	init'ed(this.canvas.scrollBarPosition)
pre	this.canvas != null
pre	this.scrollBar != null
presumption	javax.swing.JScrollBar:getValue(...)@389 <= 4_294_967_285
post	this.canvas.scrollBarPosition >= -2_147_483_638
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPane:isVisible
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:repaint
unanalyzed	call on javax.swing.JScrollBar:setValue

void pageUp()

Kind	Annotation Text
pre	(soft) this.canvas.textPane != null
pre	init'ed(this.canvas.scrollBarPosition)
pre	this.canvas != null
pre	this.scrollBar != null
presumption	javax.swing.JScrollBar:getValue(...)@396 >= -2_147_483_638
post	this.canvas.scrollBarPosition <= 4_294_967_285
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPane:isVisible
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:repaint
unanalyzed	call on javax.swing.JScrollBar:setValue

void repaintNeeded()

Kind	Annotation Text
pre	this.canvas != null

void setScrollBarMax(int)

Kind	Annotation Text
pre	(soft) init'ed(this.canvas.scrollBarPosition)
pre	(soft) this.canvas != null
pre	(soft) this.canvas.textPane != null
pre	this.document != null
pre	this.document.lines != null
pre	this.scrollBar != null
presumption	getNumLines(...)@149 - linesAllowed in range
presumption	getNumLines(...)@149 in range
presumption	java.util.List:size(...)@78 - linesAllowed in {-2³¹+1..2³²}
presumption	java.util.List:size(...)@78 >= -2³¹+1
post	init'ed(this.canvas.scrollBarPosition)
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPane:isVisible
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:repaint
unanalyzed	call on java.util.List:size
unanalyzed	call on javax.swing.JScrollBar:setValue
test_vector	java.util.List:size(...)@78 - linesAllowed: {0}, {-2³¹+1..-1, 1..2³²}
test_vector	java.util.List:size(...)@78: {-2³¹+1..0, 2..2³²-1}, {1}
test_vector	javax.swing.JScrollBar:getValueIsAdjusting(... )@164: {1}, {0}

void setScrollBarPosition(int)

Kind	Annotation Text
pre	(soft) this.canvas.textPane != null
pre	init'ed(this.canvas.scrollBarPosition)
pre	this.canvas != null
pre	this.scrollBar != null
post	init'ed(this.canvas.scrollBarPosition)
post	this.canvas.scrollBarPosition == One-of{old this.canvas.scrollBarPosition, position}
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPane:isVisible
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:repaint

void setSelectedTexT(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
pre	this.canvas != null
post	init'ed(new LinePosition(setSelectedRange#1). endLine)
post	init'ed(new LinePosition(setSelectedRange#1). endPos)
post	init'ed(new LinePosition(setSelectedRange#1). startLine)
post	init'ed(new LinePosition(setSelectedRange#1). startPos)
post	new LinePosition(setSelectedRange#1) num objects == 1
post	new LinePosition(setSelectedRange#1).endLine == position.endLine
post	new LinePosition(setSelectedRange#1).endPos == position.endPos
post	new LinePosition(setSelectedRange#1).startLine == position.startLine
post	new LinePosition(setSelectedRange#1).startPos == position.startPos
post	this.canvas.selection == &new LinePosition(setS electedRange#1)
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:isVisible
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:repaint

void trim(int)

Kind	Annotation Text
pre	(soft) init'ed(this.canvas.selection.endLine)
pre	(soft) init'ed(this.canvas.selection.endPos)
pre	(soft) init'ed(this.canvas.selection.startLine)
pre	(soft) init'ed(this.canvas.selection.startPos)
pre	(soft) this.canvas != null
pre	(soft) this.canvas.selection != null
pre	(soft) this.document.listeners != null
pre	this.document != null
pre	this.document.lines != null
presumption	java.util.List:size(...)@78 - numLines in {-2³¹..2³²-1}
presumption	selectedRange.endLine - (java.util.List:size(... )@78 - numLines) in {-2³¹.. 2³²-1}
presumption	selectedRange.startLine - (java.util.List:size(... )@78 - numLines) in {-2³¹.. 2³²-1}
post	init'ed(new LinePosition(setSelectedRange#1). endPos)
post	init'ed(new LinePosition(setSelectedRange#1). startPos)
post	new LinePosition(setSelectedRange#1) num objects <= 1
post	new LinePosition(setSelectedRange#1).endLine >= 0
post	new LinePosition(setSelectedRange#1).startLine >= 0
post	this.canvas.selection != null
post	this.canvas.selection == One-of{old this.canvas.selection, &new LinePosition(setSe lectedRange#1)}
unanalyzed	call on com.dmdirc.addons.ui_swing.UIUtilities:invo keLater
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPane:isVisible
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 fireTrimmed
unanalyzed	call on getNumLines
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.List:remove
unanalyzed	call on java.util.List:size
unanalyzed	call on javax.swing.JScrollBar:getValue
unanalyzed	call on javax.swing.JScrollBar:getValueIsAdjusting
unanalyzed	call on javax.swing.JScrollBar:setMaximum
unanalyzed	call on javax.swing.JScrollBar:setValue
unanalyzed	call on javax.swing.event.EventListenerList:getList enerList
unanalyzed	call on trimmed

void trimmed(int)

Kind	Annotation Text
pre	(soft) init'ed(this.canvas.scrollBarPosition)
pre	(soft) this.canvas.textPane != null
pre	this.canvas != null
pre	this.document != null
pre	this.document.lines != null
pre	this.scrollBar != null
post	init'ed(this.canvas.scrollBarPosition)
unanalyzed	call on com.dmdirc.addons.ui_swing.UIUtilities:invo keLater
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPane:isVisible
unanalyzed	call on com.dmdirc.addons.ui_swing.textpane. TextPaneCanvas:repaint
unanalyzed	call on getNumLines
unanalyzed	call on java.util.List:size
unanalyzed	call on javax.swing.JScrollBar:getValue
unanalyzed	call on javax.swing.JScrollBar:getValueIsAdjusting
unanalyzed	call on javax.swing.JScrollBar:setMaximum
unanalyzed	call on javax.swing.JScrollBar:setValue

void updateUI()

Kind	Annotation Text
unanalyzed	call on javax.swing.plaf.ComponentUI