Extending the project explorer

Introduction

The purpose of this page is to describe how to extend the Event-B project explorer. It covers on the one hand, the definition of the extension, and on the other hand its implementation. The Event-B project explorer is itself an implementation of the extension-point org.eclipse.ui.views. The corresponding view id is fr.systerel.explorer.navigator.view and it is over this view that we will extend the project explorer.

The useful extension points are listed below; they offer the possibility to contribute to the static checker:

• org.eclipse.ui.navigator.navigatorContent
• org.eclipse.ui.navigator.viewer

Before Starting

It is necessary to define the static checked elements that are similar to the unchecked elements. We will use as an example the decompositionFile that is defined as follows:

• decompositionFile
  • decompositionRoot
    • Component(machine to be decomposed)
    • Configuration(style:shared event/shared variables;newProjectOption:decompose in the same project/different projects;decomposeContextOption:noDecomposition/minimal decomposition)
    • SubComponent(resulting decomposed parts)
      • SubComponentElement(elements used to decompose:variables for shared event and events for shared variable)

Navigator Content

A content extension provides a content and label provider that can be used by a navigator content service (Event-B project explorer). The navigatorContent extension defines the specific classes for the content provider, label provider, and action provider in addition to the types of elements the extension knows about.

• some dependency extractors
• the tool itself

Declaration

The autoTools extension-point allows tool writers to register their tool implementation under a symbolic name that is then used by the Rodin platform to find and run the tool. The symbolic name is the id of the tool extension. An example of the implementation of a static checker can be seen as follows:

<extension
       point="org.rodinp.core.autoTools">
    <tool
          class="ch.ethz.eventb.decomposition.internal.core.sc.DecompositionStaticChecker"
          id="decompositionSC"
          name="Decomposition Static Checker">
       <extractor
             class="ch.ethz.eventb.decomposition.internal.core.sc.DecompositionStaticChecker"
             name="Decomposition Extractor of Static Checker">
          <inputType
                id="ch.ethz.eventb.decomposition.core.dcpFile">
          </inputType>
       </extractor>
    </tool>
 </extension>

We defined a static checker tool that will run for the inputType defined (ch.ethz.eventb.decomposition.core.dcpFile). The class provided for extractors must implement the org.rodinp.core.builder.IExtractor interface, while the class provided for tools themselves must implement org.rodinp.core.builder.IAutomaticTool. The Rodin platform itself does not provide any automatic tools. These are provided by additional features such as the Event-B modelling environment (see plugin org.eventb.core).

Programmatic usage

The class to be implement usually extends the class org.eventb.core.sc.StaticChecker and needs to implement the abstract method ‘extract()‘ from the interface org.rodinp.core.builder.IExtractor:

    public void extract(IFile file, IGraph graph, IProgressMonitor monitor)throws CoreException {
        try {
              monitor.beginTask(Messages.bind(Messages.build_extracting, file.getName()), 1);
              IRodinFile source = RodinCore.valueOf(file);
              IDecompositionRoot root = (IDecompositionRoot) source.getRoot();
              IRodinFile target = root.getSCDecompositionRoot().getRodinFile();
              graph.addTarget(target.getResource());
              graph.addToolDependency(source.getResource(), target.getResource(),true);
           } finally {
              monitor.done();
           }
    }

An org.rodinp.core.builder.IGraph interface is used by the extractors registers with the builder to manipulate the dependency graph of all Rodin resources of a Rodin project. It is a Facade to the more complicated ways of manipulating the dependency graph inside the builder. Some information is cached in the corresponding object so the contents of the facade must be synchronised with the graph at the end of an extraction. Requests to add nodes to the graph must be made explicitly by methods addNode(). Dependencies are managed by the facade. This saves clients from having to compute dependency graph deltas themselves.

We have already defined the static check tool and the target for which it will run. Now, we need to configure the static checker tool. It is necessary to define the checks that are required for each element and that is done by adding an extension-point of org.eventb.core.configurations.

== Example ==

Navigator Viewer

Programmatic usage

== Example ==

This information becomes deprecated with Rodin 0.9.2

The project explorer allows the registration of new file types that should be displayed.

This Demo Plug-in (mirror) demonstrates how to extend the project explorer. After installation, the plug-in shows static checked models and their variables inside the explorer.

Note, that this is for demonstration only! We selected the static checked files, because we do not want to spoil the project explorer extension with a lot of overhead to define our own file types.