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.