Extending the Rodin Structured Editor (How to extend Rodin Tutorial)

<prev: Extend the database

^up: How to extend Rodin Tutorial (Index)

In this part

We will use the extension points provided by the plugin org.eventb.ui to add our Probabilistic Attribute on events and the Bound Element to the Structured Editor.

Step 1

To structure a bit our development, we will separate the UI from the business layer.
1. Create a new plugin (here fr.systerel.rodinextension.sample.ui, and this time, select "This plug-in will make contributions to the UI" as it will be indeed the case here.
2. Add our business plugin (fr.systerel.rodinextension.sample) to the dependencies as well as org.eventb.ui that provides the extensions points we want to use.

Step 2

1. Add the extension point org.eventb.ui.editorItems At this point, we will start to add our extensions to the structured editor.

Step 3

First, let's add the probabilistic attribute to Event-B events.
The probabilistic attribute can have two values : 'standard' (by default) and 'probabilistic'. Thus we need to create a 'choiceAttribute' extension. Create a new 'choice attibute' extension :
1. give a unique ID to identify this attribute in the UI plugin (such as fr.systerel.rodinextension.sample.ui.probabilistic),
2. in typeID, give the ID reference of the probabilistic attribute in our business plugin (here fr.systerel.rodinextension.sample.probabilistic),
3. create a class (using Eclipse assist, see Step4) to manipulate this attribute, this class should implements the interface org.eventb.ui.IAttributeManipulation.

This class should be implemented the following :

Before doing any manipulation of the given IRodinElement, we have to cast this element as an IInternalElement (interface from org.rodinp.core providing access to element attributes. As we know that the element that will carry the probabilistic attribute is of type IEvent, and as IEvent implements the interface IInternalElement, let's create the following method.

 	private IEvent asEvent(IRodinElement element) {
		assert element instanceof IEvent;
		return (IEvent) element;
	}

We also have to add the ID of the probabilistic attribute as a constant, as we will need it at various places in this class. We then add the following code :

 public static IAttributeType.Boolean PROB_ATTRIBUTE = RodinCore
			.getBooleanAttrType(QualProbPlugin.PLUGIN_ID + ".probabilistic");

where IAttributeType.Boolean defines that our probabilistic attribute is actually coded as a boolean. We will implement the probabilistic attribute as followed :

if the event is probabilistic, the probabilistic attribute is set to true,

otherwise, the event is standard (e.g. non probabilistic) so the probabilistic attribute is set to false.

There are several Types for attributes. See here from more details. //FIXME insert a link to IAttributeType doc

Now let's fill the methods required to implement IAttributeManipulation :

1. getPossibleValues(IRodinElement element, IProgressMonitor monitor) should return an array of two constant values : 'standard' and 'probabilistic',

2. getValue(IRodinElement element, IProgressMonitor monitor) should 'convert' the given element as an event (using asEvent) and return the value (retrieved by IInternalElement.getAttributeValue(PROB_ATTRIBUTE) corresponding to the state of the probabilistic attribute.(e.g. should return 'probabilistic' if the attribute has value true, false otherwise.

3. hasValue(IRodinElement element, IProgressMonitor monitor) should check if the given element converted as an event has a probabilistic attribute using the method IInternalElement.hasAttribute(PROB_ATTRIBUTE)

4. removeAttribute(IRodinElement element, IProgressMonitor monitor) should convert the given element as an event, and use IInternalElement.removeAttribute(PROB_ATTRIBUTE, monitor);

5. setDefaultValue(IRodinElement element, IProgressMonitor monitor) should convert the given element as an event, and do IInternalElement.setAttributeValue(PROB_ATTRIBUTE, false, monitor); as the default value for the probabilistic attribute is false,

6. finally, setValue(IRodinElement element, String value, IProgressMonitor monitor) should check that the given value correspond to the "probabilistic" string constant, and set the value of the element (previously converted as an event) to true if it is the case, or set the value to false otherwise.

<prev: Extend the database

^up: How to extend Rodin Tutorial (Index)