method

com.dmdirc.addons.ui_swing.actions.PasteAction__ static_init

method	void com.dmdirc.addons.ui_swing.actions. PasteAction(JTextComponent)
post	this.comp == comp
post	init'ed(this.comp)

method	void actionPerformed(ActionEvent)
pre	this.comp != null

method	bool isEnabled()
pre	this.comp != null
presumption	java.awt.Toolkit:getDefaultToolkit(...)@73 != null
presumption	java.awt.Toolkit:getSystemClipboard(...)@73 != null
presumption	java.awt.datatransfer.Clipboard:getContents(... )@73 != null
presumption	init'ed(java.awt.datatransfer.DataFlavor. stringFlavor)
post	init'ed(return_value)
test_vector	javax.swing.text.JTextComponent:isEditable(... )@72: {0}, {1}
test_vector	javax.swing.text.JTextComponent:isEnabled(...)@72: {0}, {1}