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 on

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

2. // FIXME Continue here.

<prev: Extend the database

^up: How to extend Rodin Tutorial (Index)