Extending the Pretty Print Page

The Petty Print Page of the Event-B Editor provides a rendered view of an edited machine or context, for an quicker and easier reading.

An example of pretty print page

As a mechanism is available to extend Rodin's Structured Editor, such a mechanism also exists in order to extend the Pretty Print Page. For each element to be displayed, a "pretty printer" is defined within the element extension of the structured editor.

We will have a look at :

• how the extensions can contribute to the pretty print page,

• how the pretty print page is created,

• how to implement pretty printers.

How to contribute to the Pretty Print Page

When contributing to the Event-B Editor, one uses the extension point org.eventb.ui.editorItems. This extension point defines extensions from which two of them have been updated in order to contribute to the pretty print page.

Those updated extensions are :

• element

element has been extended with a child called prettyPrinter where the name of the class that will be used to pretty print the element in the pretty print view shall be given. This class must moreover implement org.eventb.ui.IElementPrettyPrinter.

• childRelation

the child element childType of a childRelation has been extended with implicitChildProvider where the name of the class that will be used to retrieve implicit children of this type in the pretty print view shall be given. The class must moreover implement org.eventb.ui.IImplicitChildProvider.

Hence, one that wants to contribute to the pretty print page for added items, must at least provide a prettyPrinter for each of those added items, and if needed, an implicitChildProvider, that will harvest the implicit children of the given type that should also be displayed.

Note: if editor items are defined without such extensions, the added items will simply not appear on the pretty print page.

How the Pretty Print Page is created

In this part, we will discribe the core algorithm for pretty printing. The core algorithm starts on the root element (such as a context or a machine) and displays its related informations. Then in a recursive loop, it traverses all sub-elements and pretty print them.

Here is the corresponding algorithm in charge of sub-elements pretty print:

traverse(Element parent)
 begin
  for all ContributionType c in parent.getChildTypes()
  do
    appendPrefixOrSpecialPrefix(c)
    for each Element e in parent.elementsOfType(c)
    do
       appendItemBeginning(e);
       prettyPrint(e);
       //recursive traverse to continue pretty printing child elements
       traverse(e);
       appendItemEnding(e);
    od
  od
 end