//}}}
//{{{ addExtension() method
/**
* Adds a text area extension, which can perform custom painting and
* tool tip handling.
* @param extension The extension
* @since jEdit 4.0pre4
*/
public void addExtension(TextAreaExtension extension) {
extensionMgr.addExtension(DEFAULT_LAYER, extension);
repaint();
} //}}}
//{{{ addExtension() method
/**
* Adds a text area extension, which can perform custom painting and
* tool tip handling.
* @param layer The layer to add the extension to. Note that more than
* extension can share the same layer.
* @param extension The extension
* @since jEdit 4.0pre4
*/
public void addExtension(int layer, TextAreaExtension extension) {
extensionMgr.addExtension(layer, extension);
repaint();
} //}}}
//{{{ removeExtension() method
/**
* Removes a text area extension. It will no longer be asked to
* perform custom painting and tool tip handling.
* @param extension The extension
* @since jEdit 4.0pre4
*/
public void removeExtension(TextAreaExtension extension) {
extensionMgr.removeExtension(extension);
repaint();
} //}}}
//{{{ getExtensions() method
/**
* Returns an array of registered text area extensions. Useful for
* debugging purposes.
* @since jEdit 4.1pre5
*/
public TextAreaExtension[] getExtensions() {
return extensionMgr.getExtensions();
} //}}}
//{{{ getToolTipText() method
/**
* Returns the tool tip to display at the specified location.
* @param evt The mouse event
*/
public String getToolTipText(MouseEvent evt) {
if ( !textArea.getBuffer().isLoaded())
return null;
return extensionMgr.getToolTipText(evt.getX(), evt.getY());
} //}}}
|