Chapter 5. The error reporting API

Table of Contents

The error reporting API is very simple. A plugin that wishes to use it must do these three things:

The classes of the error reporting API, and the ErrorList plugin itself handle the rest automatically; displaying errors in a list, error highlighting, and so on.

Specifying dependencies

In order to give the user a helpful error message if the ErrorList plugin is not installed, your plugin should specify dependency properties. If your plugin's core class is named MyPlugin, the corresponding dependencies might look like so:

plugin.MyPlugin.depend.0=jedit 04.00.01.00
plugin.MyPlugin.depend.2=plugin ErrorListPlugin 1.2

Note that the current version of the ErrorList plugin requires jEdit 4.0pre1 or later, so your plugin should also require at least that jEdit version. If a newer version of the ErrorList plugin is available, you can specify higher version numbers than in the example above. However, all the API calls in this chapter are guaranteed to work with the above version, so in most cases you shouldn't worry about it.