Extending the Structure Editor
The "edit" view is mainly a tree with elements as nodes and attributes as value for nodes. The Extension Point is org.eventb.ui.editorItems So, each new internal element should be map to a "element" (=configuration of the display). After elements should be placed in the tree with a childRelation (=where the element appear) and each attribute of the internal element should be placed with a attributeRelation (=where the attribut appear)
Example
Below an example defining something like an invariant
<extension point="org.eventb.ui.editorItems"> <element defaultColumn="1" prefix="LABEL IN THE EDIT VIEW" typeId="com.yourOffice.pluginName.elementName"> </element> <childRelation parentTypeId="org.eventb.core.machineFile"> <childType typeId="com.yourOffice.pluginName.elementName" priority="40"> </childType> </childRelation> <attributeRelation elementTypeId="com.yourOffice.pluginName.elementName"> <attributeReference column="0" descriptionId="org.eventb.ui.label"> </attributeReference> <attributeReference column="1" descriptionId="org.eventb.ui.predicate"> </attributeReference> <attributeReference descriptionId="org.eventb.ui.isTheorem"> </attributeReference> <attributeReference descriptionId="org.eventb.ui.comment"> </attributeReference> </attributeRelation> <autoNaming attributeDescriptionId="org.eventb.ui.identifier" elementTypeId="com.yourOffice.pluginName.elementName" namePrefix="foo"> </autoNaming> </extension>
Adding a New Element
Adding a New Attribute
The extension point org.rodinp.core.attributeTypes
is used to declare a new displaying/editing a new attribute in the Structure Editor. There are two steps for doing this: first, How the attribute is going to be displayed/edited and second, the relationship between the attribute and internal elements.