Extending the Structure Editor

From Event-B
Jump to navigationJump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

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