Difference between revisions of "Extending the Rodin Structured Editor (How to extend Rodin Tutorial)"

From Event-B
Jump to navigationJump to search
imported>Pascal
imported>Pascal
Line 2: Line 2:
  
 
=== In this part ===
 
=== In this part ===
We will use the extension points provided by the plugin <tt>org.eventb.ui</tt> to add our Probabilistic Attribute on events and the Bound Element to the Structured Editor.
+
We will use the extension points provided by the plug-in <tt>org.eventb.ui</tt> to add our Probabilistic Attribute on events and the Bound Element to the Structured Editor.
  
 
=== Step 1 ===
 
=== Step 1 ===
 
To structure a bit our development, we will separate the UI from the business layer.<br>
 
To structure a bit our development, we will separate the UI from the business layer.<br>
1. Create a new plugin (here <tt>fr.systerel.rodinextension.sample.ui</tt>, and this time, select "This plug-in will make contributions to the UI" as it will be indeed the case here.<br>
+
1. Create a new plug-in (here <tt>fr.systerel.rodinextension.sample.ui</tt>, and this time, select "This plug-in will make contributions to the UI" as it will be indeed the case here.<br>
2. Add our business plugin (<tt>fr.systerel.rodinextension.sample</tt>) to the dependencies as well as <tt>org.eventb.ui</tt> that provides the extensions points we want to use.
+
2. Add our business plug-in (<tt>fr.systerel.rodinextension.sample</tt>) to the dependencies as well as <tt>org.eventb.ui</tt> that provides the extensions points we want to use.
  
 
=== Step 2 ===
 
=== Step 2 ===
Line 16: Line 16:
 
First, let's add the probabilistic attribute to Event-B events.<br>
 
First, let's add the probabilistic attribute to Event-B events.<br>
 
The probabilistic attribute can have two values : 'standard' (by default) and 'probabilistic'. Thus we need to create a 'choiceAttribute' extension.
 
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 :<br>
+
Create a new 'choice attribute' extension:<br>
1. give a unique ID to identify this attribute in the UI plugin (such as <tt>fr.systerel.rodinextension.sample.ui.probabilistic</tt>),<br>
+
1. Give a unique ID to identify this attribute in the UI plug-in (such as <tt>fr.systerel.rodinextension.sample.ui.probabilistic</tt>).<br>
2. in typeID, give the ID reference of the probabilistic attribute in our business plugin (here <tt>fr.systerel.rodinextension.sample.probabilistic</tt>), <br>
+
2. In typeID, give the ID reference of the probabilistic attribute in our business plug-in (here <tt>fr.systerel.rodinextension.sample.probabilistic</tt>).<br>
3. set the ''required'' attribute to <tt>true</tt> as we want this attribute to appear by default in the structured editor when editing events,<br>
+
3. Set the ''required'' attribute to <tt>true</tt> as we want this attribute to appear by default in the structured editor when editing events.<br>
4. create a class (using Eclipse assist, see [[Extend_Rodin_database_(How_to_extend_Rodin_Tutorial)|Step4]]) to manipulate this attribute, this class should implements the interface <tt>org.eventb.ui.IAttributeManipulation</tt>.
+
4. Create a class (using Eclipse assist, see [[Extend_Rodin_database_(How_to_extend_Rodin_Tutorial)|Step4]]) to manipulate this attribute; this class should implements the interface <tt>org.eventb.ui.IAttributeManipulation</tt>.
:This class should be implemented the following :
+
//FIXME: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 <tt>org.rodinp.core</tt> 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 <tt>IInternalElement</tt>, let's create the following method.
+
:Before doing any manipulation of the given <tt>IRodinElement</tt>, we have to cast this element as an <tt>IInternalElement</tt> (interface from <tt>org.rodinp.core</tt> providing access to element attributes. As we know that the element that will carry the probabilistic attribute is of type <tt>IEvent</tt>, and as <tt>IEvent</tt> implements the interface <tt>IInternalElement</tt>, let's create the following method.
  
 
   private IEvent asEvent(IRodinElement element) {
 
   private IEvent asEvent(IRodinElement element) {
Line 28: Line 28:
 
  return (IEvent) element;
 
  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 :
+
: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
 
   public static IAttributeType.Boolean PROB_ATTRIBUTE = RodinCore
 
  .getBooleanAttrType(QualProbPlugin.PLUGIN_ID + ".probabilistic");
 
  .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 :
+
where <tt>IAttributeType.Boolean</tt> 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 <tt>true</tt>,
 
: if the event is probabilistic, the probabilistic attribute is set to <tt>true</tt>,
 
: otherwise, the event is standard (e.g. non probabilistic) so the probabilistic attribute is set to <tt>false</tt>.
 
: otherwise, the event is standard (e.g. non probabilistic) so the probabilistic attribute is set to <tt>false</tt>.
Line 40: Line 40:
  
 
:Now let's fill the methods required to implement <tt>IAttributeManipulation</tt> :
 
:Now let's fill the methods required to implement <tt>IAttributeManipulation</tt> :
:1. getPossibleValues(IRodinElement element, IProgressMonitor monitor) should return an array of two constant values : 'standard' and 'probabilistic',<br>
+
:1. <tt>getPossibleValues(IRodinElement element, IProgressMonitor monitor)</tt> should return an array of two constant values : 'standard' and 'probabilistic'.<br>
:2. getValue(IRodinElement element, IProgressMonitor monitor) should 'convert' the given element as an event (using asEvent) and return the value (retrieved by <tt>IInternalElement.getAttributeValue(PROB_ATTRIBUTE)</tt> corresponding to the state of the probabilistic attribute.(e.g. should return 'probabilistic' if the attribute has value <tt>true</tt>, <tt>false</tt> otherwise.<br>
+
:2. <tt>getValue(IRodinElement element, IProgressMonitor monitor)</tt> should 'convert' the given element as an event (using <tt>asEvent</tt>) and return the value (retrieved by <tt>IInternalElement.getAttributeValue(PROB_ATTRIBUTE)</tt> corresponding to the state of the probabilistic attribute.(e.g. should return 'probabilistic' if the attribute has value <tt>true</tt>, <tt>false</tt> otherwise.<br>
:3. hasValue(IRodinElement element, IProgressMonitor monitor) should check if the given element converted as an event has a probabilistic attribute using the method <tt>IInternalElement.hasAttribute(PROB_ATTRIBUTE)</tt><br>
+
:3. <tt>hasValue(IRodinElement element, IProgressMonitor monitor)</tt> should check if the given element converted as an event has a probabilistic attribute using the method <tt>IInternalElement.hasAttribute(PROB_ATTRIBUTE)</tt>.<br>
:4. removeAttribute(IRodinElement element, IProgressMonitor monitor) should convert the given element as an event, and use <tt>IInternalElement.removeAttribute(PROB_ATTRIBUTE, monitor);</tt><br>
+
:4. <tt>removeAttribute(IRodinElement element, IProgressMonitor monitor)</tt> should convert the given element as an event, and use <tt>IInternalElement.removeAttribute(PROB_ATTRIBUTE, monitor)</tt>.<br>
:5. setDefaultValue(IRodinElement element, IProgressMonitor monitor) should convert the given element as an event, and do <tt>IInternalElement.setAttributeValue(PROB_ATTRIBUTE,</tt> '''false'''<tt>, monitor);</tt> as the default value for the probabilistic attribute is '''false''',<br>
+
:5. <tt>setDefaultValue(IRodinElement element, IProgressMonitor monitor)</tt> should convert the given element as an event, and do <tt>IInternalElement.setAttributeValue(PROB_ATTRIBUTE,</tt> '''false'''<tt>, monitor);</tt> as the default value for the probabilistic attribute is '''false'''.<br>
: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 <tt>true</tt> if it is the case, or set the value to <tt>false</tt> otherwise.
+
:6. finally, <tt>setValue(IRodinElement element, String value, IProgressMonitor monitor)</tt> 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 <tt>true</tt> if it is the case, or set the value to <tt>false</tt> otherwise.
  
Now we will add this attribute to events. To do so, we need to create an attribute relation that will link our probabilistic attribute to events. Return to the MANIFEST.MF extensions page<br>
+
Now we will add this attribute to events. To do so, we need to create an attribute relation that will link our probabilistic attribute to events. Return to the MANIFEST.MF extensions page.<br>
1. create a new ''attributeRelation'' extension from the <tt>org.eventb.ui.editorItems</tt> extension point.<br>
+
1. Create a new ''attributeRelation'' extension from the <tt>org.eventb.ui.editorItems</tt> extension point.<br>
2. enter <tt>org.eventb.core.event</tt> as ''elementTypeId'' in the attribute relation. This means that events will hold an attribute,<br>
+
2. Enter <tt>org.eventb.core.event</tt> as ''elementTypeId'' in the attribute relation. This means that events will hold an attribute.<br>
3. from this extension specify that the attribute held by events (among others) will be our probabilistic attribute by adding an ''attributeReference'' with the ID of our UI extension for the probabilistic attribute (here <tt>fr.systerel.rodinextension.sample.ui.probabilistic</tt>).
+
3. From this extension specify that the attribute held by events (among others) will be our probabilistic attribute by adding an ''attributeReference'' with the ID of our UI extension for the probabilistic attribute (here <tt>fr.systerel.rodinextension.sample.ui.probabilistic</tt>).
  
 
=== Step 4 ===
 
=== Step 4 ===
Line 56: Line 56:
 
This step differs from the previous, as our element Bound is a new element (e.g. not an attribute). We want it to appear at top level in the structured editor, in the same way that are elements such as invariants, events, etc.
 
This step differs from the previous, as our element Bound is a new element (e.g. not an attribute). We want it to appear at top level in the structured editor, in the same way that are elements such as invariants, events, etc.
  
We will then :  
+
We will then:  
# register the Bound element as an UI element (e.g. a new type of element),
+
# Register the Bound element as an UI element (e.g. a new type of element).
# set this element to be a 'child' of machine elements (e.g. Bound will belong to machine files),
+
# Set this element to be a 'child' of machine elements (e.g. Bound will belong to machine files).
# set up a link to edit expressions of the Bound element in the UI. (Bound element carry one expression [they extend IExpressionElement]).
+
# Set up a link to edit expressions of the Bound element in the UI. (Bound element carry one expression [they extend <tt>IExpressionElement</tt>]).
# set up a link to edit comments of the Bound element in the UI. (Bound element carry one comment [they extend ICommentedElement]).
+
# Set up a link to edit comments of the Bound element in the UI. (Bound element carry one comment [they extend <tt>ICommentedElement</tt>]).
  
 
1. To register the Bound element in the UI, create an extension 'element':
 
1. To register the Bound element in the UI, create an extension 'element':
:- in typeId, specify the ID of the extension Bound in our business plugin (here <tt>fr.systerel.rodinextension.sample.bound</tt>)
+
:- In typeId, specify the ID of the extension Bound in our business plug-in (here <tt>fr.systerel.rodinextension.sample.bound</tt>).
:- in imagePath, you can specify the icon to be displayed next to the element (we created here a folder 'icons' containing an default icon)
+
:- In imagePath, you can specify the icon to be displayed next to the element (we created here a folder 'icons' containing an default icon).
:- in prefix, type 'BOUND', this value will appear as the header of bound elements in the structured editor,
+
:- In prefix, type 'BOUND', this value will appear as the header of bound elements in the structured editor.
:- in 'defaultColumn' field, put the value '0' as to make the Bound element appear at top level in the outline of machines.
+
:- In 'defaultColumn' field, put the value '0' as to make the Bound element appear at top level in the outline of machines.
  
2. To set Bound element to be a child element of a machine
+
2. To set Bound element to be a child element of a machine:
:- create an extension 'childRelation' using the extension point <tt>org.eventb.ui.editorItems</tt>,<br>
+
:- Create an extension 'childRelation' using the extension point <tt>org.eventb.ui.editorItems</tt>.<br>
:- in ''parentTypeId'' field of this extension, enter "<tt>org.eventb.core.machineFile</tt>" to refer to machine files,<br>
+
:- In ''parentTypeId'' field of this extension, enter "<tt>org.eventb.core.machineFile</tt>" to refer to machine files.<br>
:- create a sub element for the child relation extension,<br>
+
:- Create a sub element for the child relation extension<br>
:- and refer to the ID of the bound in our business class (here <tt>fr.systerel.rodinextension.sample.bound</tt>),<br>
+
:- and refer to the ID of the bound in our business class (here <tt>fr.systerel.rodinextension.sample.bound</tt>).<br>
:- put a priority of '65' to display Bound elements after ''variants'' but before ''events''. (Have a look at the ''childRelation'' for <tt>org.eventb.core.machineFile</tt> type in extension <tt>org.eventb.ui.editorItems</tt> of the package <tt>org.eventb.ui</tt> to view the priorities of other elements displayed in the structured editor).
+
:- Put a priority of '65' to display Bound elements after ''variants'' but before ''events''. (Have a look at the ''childRelation'' for <tt>org.eventb.core.machineFile</tt> type in extension <tt>org.eventb.ui.editorItems</tt> of the package <tt>org.eventb.ui</tt> to view the priorities of other elements displayed in the structured editor).
  
3. To set up a link to edit the expression of a Bound element :
+
3. To set up a link to edit the expression of a Bound element:
:- create an extension ''attributeRelation'' for our elementTypeId <tt>fr.systerel.rodinextension.sample.bound</tt>,
+
:- Create an extension ''attributeRelation'' for our elementTypeId <tt>fr.systerel.rodinextension.sample.bound</tt>.
:- add one ''attributeReference'' to <tt>org.eventb.ui.expression</tt> (descriptionID).
+
:- Add one ''attributeReference'' to <tt>org.eventb.ui.expression</tt> (descriptionID).
  
4. To set up a link to edit the comment of a Bound element :
+
4. To set up a link to edit the comment of a Bound element:
:- repeat addition of an ''attributeReference'' to the above ''attributeRelation'' but specifying <tt>org.eventb.ui.expression</tt> as descriptionID.
+
:- Repeat addition of an ''attributeReference'' to the above ''attributeRelation'' but specifying <tt>org.eventb.ui.expression</tt> as descriptionID.
  
You can now launch a Rodin product with our plugins imported and see the result :
+
You can now launch a Rodin product with our plug-ins imported and see the result:
  
 
[[Image:Extend_Rodin_Tuto_1_8_Used_ExtensionsExtended_UI.png]]
 
[[Image:Extend_Rodin_Tuto_1_8_Used_ExtensionsExtended_UI.png]]
Line 88: Line 88:
 
Congratulations! You are now able to edit the elements you added in Rodin Database.
 
Congratulations! You are now able to edit the elements you added in Rodin Database.
  
{{Navigation|Previous= [[Extend_Rodin_database_(How_to_extend_Rodin_Tutorial)|Extend the database]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= }}
+
{{Navigation|Previous= [[Extend_Rodin_database_(How_to_extend_Rodin_Tutorial)|Extending the database]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= }}
  
 
[[Category:Developer documentation|*Index]]
 
[[Category:Developer documentation|*Index]]
 
[[Category:Rodin Platform|*Index]]
 
[[Category:Rodin Platform|*Index]]
 
[[Category:Tutorial|*Index]]
 
[[Category:Tutorial|*Index]]

Revision as of 14:30, 20 August 2010

In this part

We will use the extension points provided by the plug-in 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 plug-in (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 plug-in (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 attribute' extension:
1. Give a unique ID to identify this attribute in the UI plug-in (such as fr.systerel.rodinextension.sample.ui.probabilistic).
2. In typeID, give the ID reference of the probabilistic attribute in our business plug-in (here fr.systerel.rodinextension.sample.probabilistic).
3. Set the required attribute to true as we want this attribute to appear by default in the structured editor when editing events.
4. Create a class (using Eclipse assist, see Step4) to manipulate this attribute; this class should implements the interface org.eventb.ui.IAttributeManipulation. //FIXME: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.

Now we will add this attribute to events. To do so, we need to create an attribute relation that will link our probabilistic attribute to events. Return to the MANIFEST.MF extensions page.
1. Create a new attributeRelation extension from the org.eventb.ui.editorItems extension point.
2. Enter org.eventb.core.event as elementTypeId in the attribute relation. This means that events will hold an attribute.
3. From this extension specify that the attribute held by events (among others) will be our probabilistic attribute by adding an attributeReference with the ID of our UI extension for the probabilistic attribute (here fr.systerel.rodinextension.sample.ui.probabilistic).

Step 4

Finally, let's add the Bound element to Event-B machines.
This step differs from the previous, as our element Bound is a new element (e.g. not an attribute). We want it to appear at top level in the structured editor, in the same way that are elements such as invariants, events, etc.

We will then:

  1. Register the Bound element as an UI element (e.g. a new type of element).
  2. Set this element to be a 'child' of machine elements (e.g. Bound will belong to machine files).
  3. Set up a link to edit expressions of the Bound element in the UI. (Bound element carry one expression [they extend IExpressionElement]).
  4. Set up a link to edit comments of the Bound element in the UI. (Bound element carry one comment [they extend ICommentedElement]).

1. To register the Bound element in the UI, create an extension 'element':

- In typeId, specify the ID of the extension Bound in our business plug-in (here fr.systerel.rodinextension.sample.bound).
- In imagePath, you can specify the icon to be displayed next to the element (we created here a folder 'icons' containing an default icon).
- In prefix, type 'BOUND', this value will appear as the header of bound elements in the structured editor.
- In 'defaultColumn' field, put the value '0' as to make the Bound element appear at top level in the outline of machines.

2. To set Bound element to be a child element of a machine:

- Create an extension 'childRelation' using the extension point org.eventb.ui.editorItems.
- In parentTypeId field of this extension, enter "org.eventb.core.machineFile" to refer to machine files.
- Create a sub element for the child relation extension
- and refer to the ID of the bound in our business class (here fr.systerel.rodinextension.sample.bound).
- Put a priority of '65' to display Bound elements after variants but before events. (Have a look at the childRelation for org.eventb.core.machineFile type in extension org.eventb.ui.editorItems of the package org.eventb.ui to view the priorities of other elements displayed in the structured editor).

3. To set up a link to edit the expression of a Bound element:

- Create an extension attributeRelation for our elementTypeId fr.systerel.rodinextension.sample.bound.
- Add one attributeReference to org.eventb.ui.expression (descriptionID).

4. To set up a link to edit the comment of a Bound element:

- Repeat addition of an attributeReference to the above attributeRelation but specifying org.eventb.ui.expression as descriptionID.

You can now launch a Rodin product with our plug-ins imported and see the result:

Extend Rodin Tuto 1 8 Used ExtensionsExtended UI.png

Congratulations! You are now able to edit the elements you added in Rodin Database.