Difference between pages "Development of a Heating Controller System" and "Extending the Pretty Print Page"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Reza
 
imported>Tommy
m
 
Line 1: Line 1:
 
{{TOCright}}
 
{{TOCright}}
==Introduction==
+
The Petty Print Page of the [[Modelling User Interface|Event-B Editor]] provides a rendered view of an edited machine or context, for an quicker and easier reading.
This section describes an Event-B development of a simple heating controller. This is a first case study that covers the entire development process; starting from a system specification and ending up in an implementation in the Ada programing language. The development process starts with an abstract specification followed by two successive refinements before decomposing the model to two separate sub-models. The refinement process continues after the first decomposition in order to arrive at a concrete level suitable for implementation. This allows us to devise an appropriate tasking structure that needed by the code generation plug-in. The outcomes of the second decomposition are a number of tasking machines plus a specific type of machine for representing protected shared data. This protected shared data facilitating communications between tasking machines. Then we illustrate how using the code generation plug-in a concurrent Ada implementation is generated. The overall aim of this case study is to put in practice the recommended methodological aspects of Event-B, particularly those aspects of modelling concerned with decomposition and code generation.
 
  
==System Architecture==
+
[[Image:PrettyPrintPage.png|480px|center|An example of pretty print page]]
  
<div id="fig:System Architecture">
+
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.
<br/>
 
[[Image:HeatingController1.jpg|center||caption text]]
 
<center>'''Figure 1''': System Architecture</center>
 
<br/>
 
</div>
 
  
 +
We will have a look at :
  
In the [[:Image:HeatingController1.jpg|System Architecture]] diagram an overview of the '''Heating Controller''' and its related components are presented. The controller in the middle of the diagram communicates inputs and outputs parameters with its surrounding components. At the top there are two buttons that allow the user to increase/decrease '''Target Temperature'''. The target temperature periodically will be sent by the controller to the related display to be shown to the outside world.
+
* how the extensions can contribute to the pretty print page,
The controller uses two '''Temperature Sensors''' to poll the environment temperature. The average of the values read from these two sensors is calculated and displayed by the controller on the '''Current Temperature Display'''. If the current temperature is ''lower'' than the target temperature, the controller will turn on the heater source using '''Heat Source Switch''', otherwise this switch will be turned off by the controller. The status of the heater itself also will be monitored through the '''Heater Sensor'''. If due to some faults the heater is not working properly, the controller will activate either of '''Over-temperature Alarm''' or '''No-heat Alarm'''
 
  
 +
* 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 <tt>org.eventb.ui.editorItems</tt>.
 +
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 :
 +
* <tt>element</tt>
 +
:<tt>element</tt> has been extended with a child called <tt>prettyPrinter</tt> 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 <tt>org.eventb.ui.IElementPrettyPrinter</tt>.
 +
 +
* <tt>childRelation</tt>
 +
:the child element <tt>childType</tt> of a <tt>childRelation</tt> has been extended with <tt>implicitChildProvider</tt> 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 <tt>org.eventb.ui.IImplicitChildProvider</tt>.
 +
 +
Hence, one that wants to contribute to the pretty print page for added items, must at least provide a <tt>prettyPrinter</tt> for each of those added items, and if needed, an <tt>implicitChildProvider</tt>, 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 (we will use the term "core pretty printer" to refer to this piece of code in the pretty print process).
 +
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:
 +
 +
<tt>
 +
''traverse(Element parent)''
 +
  begin
 +
  for all ContributionType c in parent.getChildTypes()
 +
  do
 +
    appendPrefixOrSpecialPrefix(c)
 +
    for each Element e in parent.elementsOfType(c)
 +
    do
 +
        '''IElementPrettyPrinter p = e.getPrettyPrinter();'''
 +
        '''p.prettyPrint(e, parent);'''
 +
        p.appendItemBeginning(e); // Used to print attributes or additional info
 +
        //recursive traverse to continue pretty printing child elements
 +
        ''traverse(e);''
 +
        p.appendItemEnding(e); // Used to print attributes or additional info
 +
    od
 +
  od
 +
  end
 +
</tt>
 +
 +
As one can see, reading this algorithm, the main method that one should implement to pretty print added items is the <tt>prettyPrint</tt> method.
 +
 +
Once all defined items are contributed to the structured editor, they should normally have if needed :
 +
* a prefix, that will be appended once for all elements of this type,
 +
* a childrenSuffix, that will be appended at the end of all elements of this type.
 +
 +
The pretty printing algorithm will handle those values if no special prefix is defined by an element pretty printer.
 +
 +
In fact, one that implements the interface for pretty printing <tt>IElementPrettyPrinter</tt> will be able to define a pretty printing method, but also auxiliary methods to tune the way elements are displayed on the Pretty Print Page.
 +
 +
'''''There are 4 methods one can implement defining a pretty printer for an element :'''''
 +
 +
<tt>
 +
void prettyPrint(IInternalElement elt, IInternalElement parent, IPrettyPrintStream ps);
 +
::(Required)This method appends the string corresponding to the pretty print of the element elt.
 +
 +
boolean appendSpecialPrefix(IInternalElement parent, String defaultPrefix, IPrettyPrintStream ps, boolean empty);
 +
::(Optional)This method appends a custom prefix, and should be used to replace the default prefix which is contributed, to be appended. It shall return true to tell the core pretty printer that a special prefix was appended, so it avoids to append the default one.
 +
 +
void appendBeginningDetails(IInternalElement elt, IPrettyPrintStream ps);
 +
::(Optional)This methods appends some details that contributors can calculate on a given element, and for which there is not representation in the data model. This method appends details before traversing the children of the given element elt, but right after having pretty printed the element elt.
 +
 +
void appendEndingDetails(IInternalElement elt, IPrettyPrintStream ps);
 +
::(Optional)This method appends some details that contributors can calculate on a given element, and for which there is no representation in the data model. This method appends details after having traversed the children of the given element elt (i.e. right after having pretty printed the children of element elt).
 +
 +
</tt>
 +
 +
NOTE : comments (viewed as attributes) are however displayed by the core pretty print algorithm, which is not the case for other attributes.(see [[#Append element attributes or details]])
 +
 +
== How to implement pretty printers (of Event-B Editor contributions) ==
 +
 +
In this part we will study concrete examples, to show how the core pretty printer is extended by contributions.
 +
 +
The pretty print page displays an HTML page. This page '''is dynamically built''' by the core pretty printer and constructed '''in a stream''' represented as an <tt>IPrettyPrintStream</tt>. As contributions define pretty printers for each element they want to display, it is needed for them to append their information in HTML language, to the stream that represents the HTML page.
 +
Fortunately, the pretty printer extension mechanism comes out with a bunch of methods available from <tt>org.eventb.ui.prettyprint.PrettyPrintUtils</tt> and others from <tt>IPrettyPrintStream</tt> or <tt>PrettyPrintAlignments</tt> in the same package <tt>org.eventb.ui.prettyprint</tt>, in order to isolate and hide (to reduce complexity), the way the HTML page is produced.
 +
In fact, '''contributors should not write any HTML code themselves,'''to prevent any page structure breackage.
 +
 +
Contributors have to :
 +
* create one or more CSS class(es) for each element they want to pretty print, contributing to <tt>style.css</tt> file in the folder org.eventb.ui.html,
 +
* use the utility methods from <tt>IPrettyPrintStream</tt> or <tt>org.eventb.ui.prettyprint.PrettyPrintUtils</tt> to access them.
 +
----
 +
=== Implementation of a simple pretty printer===
 +
Let's study the implementation of the CarrierSetsPrettyPrinter.
 +
This pretty printer is available in the package <tt>org.eventb.internal.ui.eventbeditor.prettyprinters</tt>.
 +
 +
[[Image:Variables prettyPrint.png]]
 +
 +
The display wanted is described by the picture above, and the corresponding implementation is the following :
 +
 +
First we want to define only the pretty print method, as no special prefix is wanted but the keyword "VARIABLES" which is already defined in the contribution for variables (see the <tt>element</tt> extension for variables using extension point <tt>org.eventb.ui.editorItems</tt>), as well as no details is needed at the beginning or ending of a displayed variable. That's why we choose here to extend the <tt>DefaultPrettyPrinter</tt>
 +
public class VariablesPrettyPrinter extends DefaultPrettyPrinter implements IElementPrettyPrinter {..}
 +
and override only the <tt>prettyPrint</tt> method which is the following :
 +
       
 +
@Override
 +
public void prettyPrint(IInternalElement elt, IInternalElement parent, IPrettyPrintStream ps) {
 +
    if (elt instanceof IVariable) {
 +
        IVariable var = (IVariable) elt;
 +
        try {
 +
          appendVariableIdentifier(ps, wrapString(var.getIdentifierString()));
 +
        } catch (RodinDBException e) {
 +
          EventBEditorUtils.debugAndLogError(e,"Cannot get the identifier string for variable "+var.getElementName());
 +
        }
 +
    }
 +
}
 +
 +
where we build the HTML string in the static method <tt>appendVariableIdentifier(ps, wrapString(var.getIdentifierString()));</tt> defined below :
 +
private static void appendVariableIdentifier(IPrettyPrintStream ps, String identifier) {
 +
    ps.appendString(identifier, //
 +
      getHTMLBeginForCSSClass(VARIABLE_IDENTIFIER, //
 +
                              HorizontalAlignment.LEFT, //
 +
                              VerticalAlignement.MIDDLE),//
 +
      getHTMLEndForCSSClass(VARIABLE_IDENTIFIER, //
 +
                              HorizontalAlignment.LEFT, //
 +
                              VerticalAlignement.MIDDLE),//
 +
      VARIABLE_IDENTIFIER_SEPARATOR_BEGIN, //
 +
      VARIABLE_IDENTIFIER_SEPARATOR_END);
 +
}
 +
 +
We can see here that the HTML is built with the <tt>IPrettyPrintStream</tt> method <tt>appendString()</tt> and that we retrieve the CSS class for variables by defining a constant
 +
private static final String VARIABLE_IDENTIFIER = "variableIdentifier";
 +
 +
and using the methods <tt>getHTMLBeginForCSSClass()</tt> and <tt>getHTMLEndForCSSClass()</tt> to retrieve the HTML/CSS code
 +
as the class is defined in the <tt>style.css</tt> file by :
 +
.variableIdentifier {font-size:16px; color:black;font-family:"Brave Sans Mono";}
 +
 +
HTML alignments are retrieved using the enumerations from <tt>org.eventb.ui.prettyprint.PrettyPrintAlignments</tt> and <tt>VARIABLE_IDENTIFIER_SEPARATOR_BEGIN</tt> and <tt>VARIABLE_IDENTIFIER_SEPARATOR_END</tt> are constants which are set to <tt>null</tt> as there is no element information after a variable identifier to display.
 +
----
 +
===Overriding the contributed prefix===
 +
 +
Now let's look at a special case of prefix overriding to show how we can prevent the core pretty printer to append the default one to the Pretty Print Page.
 +
 +
[[Image:GuardWhereWhen.png]]
 +
 +
The figure above shows that we display the special keyword "WHEN" instead of "WHERE", the default one, when no parameters are bound to the event, and there are guards.
 +
 +
We will then implement the method <tt>appendSpecialPrefix()</tt> in the guard pretty printer class as the following :
 +
@Override
 +
  public boolean appendSpecialPrefix(IInternalElement parent, String defaultKeyword, IPrettyPrintStream ps, boolean empty) {
 +
    if (empty) {
 +
        return false;
 +
    }
 +
    try {
 +
        final List<IParameter> params = UIUtils.getVisibleChildrenOfType(parent, IParameter.ELEMENT_TYPE);
 +
          if (params.size() == 0) {
 +
              ps.appendKeyword("WHEN");
 +
          } else {
 +
              ps.appendKeyword(defaultKeyword);
 +
          }
 +
    } catch (RodinDBException e) {
 +
      EventBEditorUtils.debugAndLogError(e, "Cannot get all guards of " + parent.getElementName());
 +
    }
 +
    return true;
 +
  }
 +
 +
This method implements a specific behaviour and prints the keyword WHEN as if the core pretty printer did, using the method <tt>appendKeyword()</tt> from IPrettyPrintStream.
 +
It is important to note that if WHEN is appended, the '''method returns <tt>true</tt>''' to prevent the core pretty printer to append the keyword WHERE.
 
----
 
----
 +
===Append element attributes or details===
  
'''Main Functionaly of the System'''
+
This section explains how to append attribute or any other information to the HTML stream.
* Provideing interface to adjust Target Temperature
 
* Displaying new Target Temperature
 
* Sensing Current Temperature
 
* Displaying Current Temperature
 
* Power on/off the Heater
 
* Sensing the Heater Status
 
* Activating/Deactivating No-Heat Alarm
 
* Activating/Deactivating Over-Heat Alarm
 
  
 +
It has been chosen to not traverse element attributes the same way as elements. The main reason motivating this, is that contributor are free to define their one semantics for the presence or absence of attributes defined for an element. A contributor also might want to tune the pretty print its own way by displaying additional informations that could be calculated on the traversed element.
 +
The responsability of pretty printing them, is then let to him.
 +
Consequently, two methods are provided by the <tt>IElementPrettyPrinter</tt> interface, in order to display such informations :
  
{|align="center" border="2" cellpadding="5" cellspacing="1"
+
void appendBeginningDetails(IInternalElement elt, IPrettyPrintStream ps);
|+ '''An Overview of the Main Variables'''
+
void appendEndingDetails(IInternalElement elt, IPrettyPrintStream ps);
!Interfaces
 
!Types
 
!Definitions
 
|-
 
|Temperature Sensors
 
|Integer
 
|Temperature in degrees Celsius
 
|-
 
|Heater Sensors
 
|Boolean
 
|True when heater is at working temperature, False otherwise
 
|-
 
|Heat Source Switch
 
|Boolean
 
|True when activated, False otherwise
 
|-
 
|No-heat Alarm
 
|Boolean
 
|True when activated, False otherwise
 
|-
 
|Over-temperature Alarm
 
|Boolean
 
|True when activated, False otherwise
 
|-
 
|Current temperature Display
 
|Integer
 
|Average temperature value in degrees Celsius
 
|-
 
|Target temperature
 
|Integer
 
|Target temperature value in degrees Celsius
 
|}
 
  
==An Overview of the System Development==
+
<tt>appendBeginningDetails()</tt> will be called by the core pretty printer, before invoking the <tt>prettyPrint()</tt> method (taking place in the core algorithm above in <tt>p.appendItemBeginning(e);</tt> [[#How the Pretty Print Page is created|see core pretty print algorithm]]).
Before starting with explaining the Event-B models for the Heater Controller it is useful to provide an overview of our development approach. In this section we demonstrate this with a diagram. Starting from the top of the diagram, it shows the most abstract model of the system or as it know as the system specification.
 
[[Image:development.jpg|center]]
 
  
==System Decomposition==
+
<tt>appendEndingDetails()</tt> will be called by the core pretty printer, after invoking the <tt>prettyPrint()</tt> method (taking place in the core algorithm above in <tt>p.appendItemEnding(e);</tt>[[#How the Pretty Print Page is created|see core pretty print algorithm]]).
  
As illustrated in the system development diagram we decompose our model in two stages.  
+
====Example of events pretty printer====
 +
As an extension <tt>attributionRelation</tt> for events has been defined. The events contain attributes <tt>extended</tt> and <tt>convergence</tt> (see the picture below).
  
===First level decomposition===
+
[[Image:EventsAttributes.png]]
 +
 
 +
We will then implement the method <tt>appendBeginningDetails()</tt> of the interface <tt>IElementPrettyPrinter</tt> to display those attributes before the children of an event are traversed.
 
   
 
   
In Event-B usually we start modelling with specifying the whole system as a closed system. This includes the system that we are intending to develop plus its surrounding environment. Therefore when our model of the system becomes big and complex it is reasonable to separate the actual system from its environment. Hence in the first stage of decomposition we decompose our model to two parts, namely the controller and the environment.
+
@Override
 +
  public void appendBeginningDetails(IInternalElement elt, IPrettyPrintStream ps) {
 +
  final IEvent evt = elt.getAncestor(IEvent.ELEMENT_TYPE);
 +
    appendExtended(evt, ps);
 +
    appendConvergence(evt, ps);
 +
}
  
[[Image:Decomp1.jpg|center]]
+
Where <tt>appendConvergence(IEvent evt, IPrettyPrintStream ps)</tt> is defined as :
 +
private static void appendConvergence(IEvent evt, IPrettyPrintStream ps) {
 +
  try {
 +
    Convergence convergence = evt.getConvergence();
 +
    ps.appendLevelBegin();
 +
    ps.appendKeyword("STATUS");
 +
    appendConvergence(ps, convergence);
 +
    ps.appendLevelEnd();
 +
  } catch (RodinDBException e) {
 +
    // Do nothing
 +
  }
 +
}
  
===Second level decomposition===
+
and where <tt>appendConvergence(ps, convergence)</tt> is defined as <tt>appendVariableIdentifier(IPrettyPrintStream ps, String identifier)</tt> described in the section [[#Implementation of a simple pretty printer]] above :
In this stage we decompose the controller to some tasks that communicating through a shared object. Note that tasks still are able to communicate with the environment directly.
+
private static void appendConvergence(IPrettyPrintStream ps, Convergence convergence) {
[[Image:Decomp2.jpg|center]]
+
  String string = "ordinary";
 +
  if (convergence == Convergence.ORDINARY) {
 +
    string = "ordinary";
 +
  } else if (convergence == Convergence.ANTICIPATED) {
 +
    string = "anticipated";
 +
  } else if (convergence == Convergence.CONVERGENT) {
 +
    string = "convergent";
 +
  }
 +
    ps.appendLevelBegin();
 +
    ps.appendString(string, getHTMLBeginForCSSClass(CONVERGENCE, HorizontalAlignment.LEFT, VerticalAlignement.MIDDLE), //
 +
                            getHTMLEndForCSSClass(CONVERGENCE, HorizontalAlignment.LEFT, VerticalAlignement.MIDDLE), //
 +
                            BEGIN_CONVERGENCE_SEPARATOR, //
 +
                            END_CONVERGENCE_SEPARATOR);
 +
    ps.appendLevelEnd();
 +
}
 +
 
 +
We use here the methods <tt>ps.appendLevelBegin()</tt> and <tt>ps.appendLevelEnd()</tt> for a finer grain control of the indentation in the HTML output.
 +
Two additional methods from the <tt>IPrettyPrintStream</tt> interface, can be used to control the level of indentation :
 +
*<tt>incrementLevel()</tt> : increments the level of indentation hold by the pretty print stream,
 +
*<tt>decrementLevel()</tt> : decrements the level of indentation hold by the pretty print stream.
 +
 
 +
We finally obtain the following display, here for the initialisation of a sample refinement :
 +
 
 +
[[Image:ExtendedConvergence.png]]
 +
----

Revision as of 09:23, 16 April 2010

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 (we will use the term "core pretty printer" to refer to this piece of code in the pretty print process). 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
       IElementPrettyPrinter p = e.getPrettyPrinter();
       p.prettyPrint(e, parent);
       p.appendItemBeginning(e); // Used to print attributes or additional info
       //recursive traverse to continue pretty printing child elements
       traverse(e);
       p.appendItemEnding(e); // Used to print attributes or additional info
    od
  od
 end

As one can see, reading this algorithm, the main method that one should implement to pretty print added items is the prettyPrint method.

Once all defined items are contributed to the structured editor, they should normally have if needed :

  • a prefix, that will be appended once for all elements of this type,
  • a childrenSuffix, that will be appended at the end of all elements of this type.

The pretty printing algorithm will handle those values if no special prefix is defined by an element pretty printer.

In fact, one that implements the interface for pretty printing IElementPrettyPrinter will be able to define a pretty printing method, but also auxiliary methods to tune the way elements are displayed on the Pretty Print Page.

There are 4 methods one can implement defining a pretty printer for an element :

void prettyPrint(IInternalElement elt, IInternalElement parent, IPrettyPrintStream ps);

(Required)This method appends the string corresponding to the pretty print of the element elt.

boolean appendSpecialPrefix(IInternalElement parent, String defaultPrefix, IPrettyPrintStream ps, boolean empty);

(Optional)This method appends a custom prefix, and should be used to replace the default prefix which is contributed, to be appended. It shall return true to tell the core pretty printer that a special prefix was appended, so it avoids to append the default one.

void appendBeginningDetails(IInternalElement elt, IPrettyPrintStream ps);

(Optional)This methods appends some details that contributors can calculate on a given element, and for which there is not representation in the data model. This method appends details before traversing the children of the given element elt, but right after having pretty printed the element elt.

void appendEndingDetails(IInternalElement elt, IPrettyPrintStream ps);

(Optional)This method appends some details that contributors can calculate on a given element, and for which there is no representation in the data model. This method appends details after having traversed the children of the given element elt (i.e. right after having pretty printed the children of element elt).

NOTE : comments (viewed as attributes) are however displayed by the core pretty print algorithm, which is not the case for other attributes.(see #Append element attributes or details)

How to implement pretty printers (of Event-B Editor contributions)

In this part we will study concrete examples, to show how the core pretty printer is extended by contributions.

The pretty print page displays an HTML page. This page is dynamically built by the core pretty printer and constructed in a stream represented as an IPrettyPrintStream. As contributions define pretty printers for each element they want to display, it is needed for them to append their information in HTML language, to the stream that represents the HTML page. Fortunately, the pretty printer extension mechanism comes out with a bunch of methods available from org.eventb.ui.prettyprint.PrettyPrintUtils and others from IPrettyPrintStream or PrettyPrintAlignments in the same package org.eventb.ui.prettyprint, in order to isolate and hide (to reduce complexity), the way the HTML page is produced. In fact, contributors should not write any HTML code themselves,to prevent any page structure breackage.

Contributors have to :

  • create one or more CSS class(es) for each element they want to pretty print, contributing to style.css file in the folder org.eventb.ui.html,
  • use the utility methods from IPrettyPrintStream or org.eventb.ui.prettyprint.PrettyPrintUtils to access them.

Implementation of a simple pretty printer

Let's study the implementation of the CarrierSetsPrettyPrinter. This pretty printer is available in the package org.eventb.internal.ui.eventbeditor.prettyprinters.

Variables prettyPrint.png

The display wanted is described by the picture above, and the corresponding implementation is the following :

First we want to define only the pretty print method, as no special prefix is wanted but the keyword "VARIABLES" which is already defined in the contribution for variables (see the element extension for variables using extension point org.eventb.ui.editorItems), as well as no details is needed at the beginning or ending of a displayed variable. That's why we choose here to extend the DefaultPrettyPrinter

public class VariablesPrettyPrinter extends DefaultPrettyPrinter implements IElementPrettyPrinter {..}

and override only the prettyPrint method which is the following :

@Override
public void prettyPrint(IInternalElement elt, IInternalElement parent,	IPrettyPrintStream ps) {
   if (elt instanceof IVariable) {
       IVariable var = (IVariable) elt;
       try {
         appendVariableIdentifier(ps, wrapString(var.getIdentifierString()));
       } catch (RodinDBException e) {
         EventBEditorUtils.debugAndLogError(e,"Cannot get the identifier string for variable "+var.getElementName());
       }
   }
}

where we build the HTML string in the static method appendVariableIdentifier(ps, wrapString(var.getIdentifierString())); defined below :

private static void appendVariableIdentifier(IPrettyPrintStream ps, String identifier) {
    ps.appendString(identifier, //
      getHTMLBeginForCSSClass(VARIABLE_IDENTIFIER, //
                              HorizontalAlignment.LEFT, //
                              VerticalAlignement.MIDDLE),//
      getHTMLEndForCSSClass(VARIABLE_IDENTIFIER, //
                              HorizontalAlignment.LEFT, //
                              VerticalAlignement.MIDDLE),//
      VARIABLE_IDENTIFIER_SEPARATOR_BEGIN, //
      VARIABLE_IDENTIFIER_SEPARATOR_END);
}

We can see here that the HTML is built with the IPrettyPrintStream method appendString() and that we retrieve the CSS class for variables by defining a constant

private static final String VARIABLE_IDENTIFIER = "variableIdentifier";

and using the methods getHTMLBeginForCSSClass() and getHTMLEndForCSSClass() to retrieve the HTML/CSS code as the class is defined in the style.css file by :

.variableIdentifier {font-size:16px; color:black;font-family:"Brave Sans Mono";}

HTML alignments are retrieved using the enumerations from org.eventb.ui.prettyprint.PrettyPrintAlignments and VARIABLE_IDENTIFIER_SEPARATOR_BEGIN and VARIABLE_IDENTIFIER_SEPARATOR_END are constants which are set to null as there is no element information after a variable identifier to display.


Overriding the contributed prefix

Now let's look at a special case of prefix overriding to show how we can prevent the core pretty printer to append the default one to the Pretty Print Page.

GuardWhereWhen.png

The figure above shows that we display the special keyword "WHEN" instead of "WHERE", the default one, when no parameters are bound to the event, and there are guards.

We will then implement the method appendSpecialPrefix() in the guard pretty printer class as the following :

@Override
  public boolean appendSpecialPrefix(IInternalElement parent, String defaultKeyword, IPrettyPrintStream ps, boolean empty) {
    if (empty) {
       return false;
    }
    try {
       final List<IParameter> params = UIUtils.getVisibleChildrenOfType(parent, IParameter.ELEMENT_TYPE);
         if (params.size() == 0) {
             ps.appendKeyword("WHEN");
         } else {
             ps.appendKeyword(defaultKeyword);
         }
    } catch (RodinDBException e) {
      EventBEditorUtils.debugAndLogError(e, "Cannot get all guards of " + parent.getElementName());
    }
   return true;
 }

This method implements a specific behaviour and prints the keyword WHEN as if the core pretty printer did, using the method appendKeyword() from IPrettyPrintStream. It is important to note that if WHEN is appended, the method returns true to prevent the core pretty printer to append the keyword WHERE.


Append element attributes or details

This section explains how to append attribute or any other information to the HTML stream.

It has been chosen to not traverse element attributes the same way as elements. The main reason motivating this, is that contributor are free to define their one semantics for the presence or absence of attributes defined for an element. A contributor also might want to tune the pretty print its own way by displaying additional informations that could be calculated on the traversed element. The responsability of pretty printing them, is then let to him. Consequently, two methods are provided by the IElementPrettyPrinter interface, in order to display such informations :

void appendBeginningDetails(IInternalElement elt, IPrettyPrintStream ps);
void appendEndingDetails(IInternalElement elt, IPrettyPrintStream ps);

appendBeginningDetails() will be called by the core pretty printer, before invoking the prettyPrint() method (taking place in the core algorithm above in p.appendItemBeginning(e); see core pretty print algorithm).

appendEndingDetails() will be called by the core pretty printer, after invoking the prettyPrint() method (taking place in the core algorithm above in p.appendItemEnding(e);see core pretty print algorithm).

Example of events pretty printer

As an extension attributionRelation for events has been defined. The events contain attributes extended and convergence (see the picture below).

EventsAttributes.png

We will then implement the method appendBeginningDetails() of the interface IElementPrettyPrinter to display those attributes before the children of an event are traversed.

@Override
 public void appendBeginningDetails(IInternalElement elt, IPrettyPrintStream ps) {
  final IEvent evt = elt.getAncestor(IEvent.ELEMENT_TYPE);
   appendExtended(evt, ps);
   appendConvergence(evt, ps);
}

Where appendConvergence(IEvent evt, IPrettyPrintStream ps) is defined as :

private static void appendConvergence(IEvent evt, IPrettyPrintStream ps) {
 try {
    Convergence convergence = evt.getConvergence();
    ps.appendLevelBegin();
    ps.appendKeyword("STATUS");
    appendConvergence(ps, convergence);
    ps.appendLevelEnd();
 } catch (RodinDBException e) {
    // Do nothing
 }
}

and where appendConvergence(ps, convergence) is defined as appendVariableIdentifier(IPrettyPrintStream ps, String identifier) described in the section #Implementation of a simple pretty printer above :

private static void appendConvergence(IPrettyPrintStream ps, Convergence convergence) {
  String string = "ordinary";
  if (convergence == Convergence.ORDINARY) {
   string = "ordinary";
  } else if (convergence == Convergence.ANTICIPATED) {
   string = "anticipated";
  } else if (convergence == Convergence.CONVERGENT) {
   string = "convergent";
  }
   ps.appendLevelBegin();
   ps.appendString(string, getHTMLBeginForCSSClass(CONVERGENCE, HorizontalAlignment.LEFT, VerticalAlignement.MIDDLE), //
                           getHTMLEndForCSSClass(CONVERGENCE, HorizontalAlignment.LEFT, VerticalAlignement.MIDDLE), //
                           BEGIN_CONVERGENCE_SEPARATOR, //
                           END_CONVERGENCE_SEPARATOR);
   ps.appendLevelEnd();
}

We use here the methods ps.appendLevelBegin() and ps.appendLevelEnd() for a finer grain control of the indentation in the HTML output. Two additional methods from the IPrettyPrintStream interface, can be used to control the level of indentation :

  • incrementLevel() : increments the level of indentation hold by the pretty print stream,
  • decrementLevel() : decrements the level of indentation hold by the pretty print stream.

We finally obtain the following display, here for the initialisation of a sample refinement :

ExtendedConvergence.png