Extending the Rodin Event-B Explorer (How to extend Rodin Tutorial)
Contents
In this part
We continue our work on the UI integration of our plug-in and extend the Event-B Explorer view. This view allows to display the structure of Event-B projects, represented as a tree. As we introduced a new element "Bound", we want it to appear in this view as any other machine element such as variables or invariants. The Event-B Explorer uses the Common Navigator Framework (extension point org.eclipse.ui.navigator), thus we will not use a Rodin extension point but directly Eclipse extension points.
What we want to get : We want our Bound element to appear in the Event-B Explorer view as a direct child (as there will be a single bound element per machine), as described in the picture below:
First, we will create Bound element contents to fill the navigator view with, and then we will bind those contents to the navigator view.
Step 1
Add a dependency to the package org.eclipse.ui.navigator (This is the required package to use the navigator extension points).
Extend org.eclipse.ui.navigator.navigatorContent (This extension point allows to extend the navigator by adding contents to it).
Step2
Add a new navigatorContent extension by using the newly added extension point org.eclipse.ui.navigator.navigatorContent. In this step, we will add two clause expressions to the navigatorContent extension to explain in which context this content shall be displayed and what to display. In the following step, we will give contents to this extension. The two clauses expressions that we will use from navigatorContent extension are:
- - triggerPoints. The triggerPoints expression defines the nodes to be used when resolving the Common Navigator content provider's getElements() or getChildren(). This is also used to select the extension for providing labels, images, descriptions and for sorting.
- - possibleChildren. The possibleChildren expression defines the node to be used when resolving the Common Navigator content provider's getParent(). It is also used to help to determine the parent when handling drop operations.
We want the navigator to display the Bound element when expanding a machine structure. Hence, we need to add a trigger calling a content provider associated to the Bound element. To do this, first, add a clause triggerPoints to the navigatorContent extension, and in this clause add a clause instanceof. Then fill the value field of the instanceof clause with org.eventb.core.IMachineRoot. By doing this, we tell the navigator to call a Bound element content provider when we want to display the children element of a machine.
Moreover, we expect Bound elements to be displayed at the top level in the Event-B explorer tree (where appears the variable "group" node, or invariants "group" node). This means that possible children for the node to be used by the navigator are Bound elements themselves. Add a clause possibleChildren to the navigatorContent extension, and add the following instanceof clause fr.systerel.rodinextension.sample.basis.IBound.
Step 3
Now let's fill the contents of our extension navigatorContent for the Bound element.
1. Give a unique ID for the content extension (here we use fr.systerel.rodinextension.sample.ui.boundContent).
2. Give a readable name for this extension of the navigator (such as "Bound Element" or "Bound Element Navigator Node").
3. The field priority is linked to the field appearsBefore. These two fields allow to define where our content extension should take place in the tree structure. We used here the lower priority, to avoid to display the Bound element at the top of the machine children hierarchy.
4. In appearsBefore, we put the fr.systerel.explorer.navigator.content.event which is the identifier of the content extension for events (To have a look at the core extensions for the contents of the navigator, go in the fr.systerel.explorer plug-in and look for navigatorContent extensions).
5. Define a new class for the content provider, implementing the interface ITreeContentProvider, to be used to display the bound element (using eclipse's "new java class wizard").
We have created one, named BoundContentProvider, and implemented as follows :
public class BoundLabelProvider implements ILabelProvider, IImageProvider {
private static final String BOUND_LABEL = "Bound";
@Override
public Image getImage(Object element) {
if (element instanceof IBound) {
return getImage();
}
return null;
}
public static Image getImage() {
final ImageRegistry reg = EventBUIPlugin.getDefault()
.getImageRegistry();
return reg.get(IEventBSharedImages.IMG_CONSTANT);
}
@Override
public String getText(Object element) {
if (element instanceof IBound) {
return BOUND_LABEL;
}
return null;
}
@Override
public ImageDescriptor getImageDescriptor(IRodinElement element) {
final Image image = getImage(element);
if (image == null) {
return null;
}
final ImageDescriptor desc = ImageDescriptor.createFromImage(image);
return desc;
}
// other methods can be ignored...
}
Methods getImage(Object element) and getText(Object element) need to be implemented from the ILabelProvider interface.
In getImage(Object element), we return the icon registered for constants, if the element is an instance of IBound (see org.eventb.ui.IEventBSharedImages to get the ID of shared images in Rodin).
In getText(Object element), we return the BOUND_LABEL constant for IBound instances, as IBound elements have no label, and there is only one bound element per machine.
Method getImageDescriptor(IRodinElement element) need to be implemented from IImageProvider interface.
We simply create a fresh descriptor using the static method ImageDescriptor.createFromImage(Image image); from the image we get from getImage(Object element).
The other methods can be ignored.
This is it. You are now able to view bound elements in the Event-B Explorer view.
