Extending the Structure Editor

From Event-B
Jump to navigationJump to search

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.

How the attribute is going to be displayed/edited

The relationship between the attribute and internal elements