Extending the Index Manager

The indexing system, that stores the data and answers requests, is separated from the indexers, that actually do the job of scanning files and adding occurrences.

So, along with existing Event-B model indexers, it is possible to have indexers for other target types, or even indexers for Event-B models that record additional information.

Making your own indexer and integrating it to the indexing system can be achieved in the following way.

Defining target file types

The first task is to define which file types your indexer will be able to index. We are speaking here of making a single indexer, but you may as well develop several indexers, each one specialized in one or more file types.

Later, to make the indexing system aware of your indexer, you will have to register it (RodinIndexer#register()), specifying the file types you are interested in. Then, each time a file of one of these types gets modified, the indexing system will call the indexer on this file.

Declaring custom occurrence kinds

Depending on the type of information your indexer will have to retrieve, you may need to define your own occurrence kinds.

For instance, Event-B indexer plug-in declares kinds DECLARATION, REFERENCE and MODIFICATION, to qualify the various occurrences of variables, carrier sets, ..., in model files (of course, not all occurrence kinds can apply to all elements !).

Occurrence kind declaration is achieved through an extension point. TODO: name the extension point

Implementing an indexer

Now, getting further towards the code, what is an indexer required to do ?

An indexer's fundamental task consists in scanning a file, declaring elements, and adding occurrences.

Indexers must implement the IIndexer interface. This interface consists in 3 methods

• getId()
• getDependencies(IInternalElement)
• index(IIndexingToolkit)

The first one merely gives the unique identifier of the indexer. The other two will do a more complex job.

Dependencies occur between files when there can be occurrences of an element outside the file of its declaration. For example, in Event-B, a carrier set can be declared in a context and referenced in a machine that sees it. In this case, it is necessary to index the declaring one before the referencing one, because an element can ever have an occurrence stored only if it has been declared before. As the indexing system has no sense of how to understand file contents, stating file dependencies is delegated to indexers (however, if it is already done by indexers that run before yours, there is no need to do it twice, simply return an empty array; see next section).

The indexing system gathers file dependencies and computes the order in which they must be indexed. If cycles are detected, they are arbitrarily broken. If no dependencies are specified, all files are indexed in no special order. Once the order is decided, the indexing system actually calls IIndexer#index().

Here comes the index method and the IIndexingToolkit object. This object has various functions. First, it gives the root element of the file to index. The file can be assumed to be of one of the types the indexer registered for. It also gives the declarations of imported elements (if any): these are the elements that were declared in files on which the current one depends, that may occur in it. If your indexer depends on others (see below), you can also get the result of their work.

So the IIndexingToolkit gives input data, but it also gets the output of your indexer. This is achieved through its declare() and addOccurrences() methods.

The imports received come from previous exportations. If elements are to be visible to indexers of dependent files (including your indexer), they must be exported before returning.

Indexing is run as a Job, so it can be canceled. Indexers are expected to check regularly for cancellation (IIndexingToolkit#isCanceled()) and return as soon as possible when it is requested.

Depending on other indexers

The architecture has been thought in order to allow several indexers to work sequentially on the same file, letting the last ones benefit from the results of the first ones. To do this, simply indicate in the indexer extension point after which indexers yours should be run. It will then be called to get file dependencies and index file elements.

If file dependencies are well specified by indexers yours depends on, there is no need to specify them again, you can just return an empty result in the corresponding method.

However, it is possible to add other dependencies. All dependencies will be taken into account together to compute the order in which files will be indexed.

The main interest of that feature is to get declarations from previous indexers(IIndexingToolkit#getDeclarations()). It is then possible to add your own specific occurrences of the elements subject of these declarations (IIndexingToolkit#addOccurrence() as usual).