Extending the Rodin Pretty Print Page (How to extend Rodin Tutorial)

<prev: Adding elements to the Event-B explorer

>next: Providing help

^up: How to extend Rodin Tutorial (Index)

In this part

As this extension mechanism is detailed on a dedicated page of the wiki, we will here comment the implementation of a pretty printer for the bound elements. Unfortunately, it is not yet possible to act on the pretty print of events, so the probabilistic will not be displayed here.

See here for the detailed documentation : Extending the Pretty print Page

Step1

Go back to the element extension for the bound element fr.systerel.rodinextension.sample.bound that we previously created from the org.eventb.ui.editorItems extension point. Create a new class that will implement the pretty printer for the bound element, using the eclipse new class wizard as in the picture below.

Step2

Edit this class as following :

public class BoundPrettyPrinter extends DefaultPrettyPrinter {

	private static final String BOUND_EXPRESSION = "variantExpression";
	private static final String BOUND_EXPRESSION_SEPARATOR_BEGIN = null;
	private static final String BOUND_EXPRESSION_SEPARATOR_END = null;

	@Override
	public void prettyPrint(IInternalElement elt, IInternalElement parent, IPrettyPrintStream ps) {
		if (elt instanceof IBound) {
			IBound bound = (IBound) elt;
			try {
				appendBoundExpression(ps,wrapString(bound.getExpressionString()));
			} catch (RodinDBException e) {
				System.err.println("Cannot get the expression string for the bound element."+ e.getMessage());
			}
		}
	}
	
	private static void appendBoundExpression(IPrettyPrintStream ps, String expression) {
	    ps.appendString(expression, //
	      getHTMLBeginForCSSClass(BOUND_EXPRESSION, //
	                              HorizontalAlignment.LEFT, //
	                              VerticalAlignement.MIDDLE),//
	      getHTMLEndForCSSClass(BOUND_EXPRESSION, //
	                              HorizontalAlignment.LEFT, //
	                              VerticalAlignement.MIDDLE),//
	                              BOUND_EXPRESSION_SEPARATOR_BEGIN, //
	                              BOUND_EXPRESSION_SEPARATOR_END);
	}

}

As we want only to display the expression hold by the Bound element, we extend here org.eventb.ui.prettyprint.DefaultPrettyPrinter to avoid implementing unused methods from the IElementPrettyPrinter interface. In fact, what we need here is only to implement the method prettyPrint(IInternalElement elt, IInternalElement parent, IPrettyPrintStream ps).

This method has to check that the handled element is a bound (e.g. instanceof IBound) and then display the embedded expression string. We created a dedicated method to append the expression in the pretty print stream, and used the pretty print helpers methods that are provided by org.eventb.ui.prettyprint.PrettyPrintUtils using the following static imports :

import static org.eventb.ui.prettyprint.PrettyPrintUtils.getHTMLBeginForCSSClass;

import static org.eventb.ui.prettyprint.PrettyPrintUtils.getHTMLEndForCSSClass;

import static org.eventb.ui.prettyprint.PrettyPrintUtils.wrapString;

The only trick here, was to use the same display as the one used by variants using private static final String BOUND_EXPRESSION = "variantExpression";. Doing so, we reuse the CSS class that is defined for variant expressions. There are many pre-defined CSS classes for the Event-B language elements. To review them, go to the file html/style.css in the plugin org.eventb.ui.

Here is the result you should get :

<prev: Adding elements to the Event-B explorer

>next: Providing help

^up: How to extend Rodin Tutorial (Index)