imported>Tommy |
|
Line 1: |
Line 1: |
− | {{Navigation|Previous= [[Extending_the_Rodin_Event-B_Explorer_(How_to_extend_Rodin_Tutorial)]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= }}
| |
| | | |
− | === 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| Extending the Pretty print Page]]
| |
− |
| |
− | === Step1 ===
| |
− | Go back to the element extension for the bound element <tt>fr.systerel.rodinextension.sample.bound</tt> that we previously created from the <tt>org.eventb.ui.editorItems</tt> 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.
| |
− |
| |
− | [[Image:Extend_Rodin_Tuto_1_11_Add_PrettyPrinter.png]]
| |
− |
| |
− | === 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 <tt>org.eventb.ui.prettyprint.DefaultPrettyPrinter</tt> to avoid implementing unsued methods from the <tt>IElementPrettyPrinter</tt> interface. In fact, what we need here is only to implement the method <tt>prettyPrint(IInternalElement elt, IInternalElement parent, IPrettyPrintStream ps)</tt>.
| |
− |
| |
− | This method has to check that the handled element is a bound (e.g. instanceof <tt>IBound</tt>) 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 <tt>org.eventb.ui.prettyprint.PrettyPrintUtils</tt> using the following static imports :<br>
| |
− | :<tt>import static org.eventb.ui.prettyprint.PrettyPrintUtils.getHTMLBeginForCSSClass;</tt>
| |
− | :<tt>import static org.eventb.ui.prettyprint.PrettyPrintUtils.getHTMLEndForCSSClass;</tt>
| |
− | :<tt>import static org.eventb.ui.prettyprint.PrettyPrintUtils.wrapString;</tt>
| |
− |
| |
− | The only trick here, was to use the same diplay as the one used by variants using <tt>private static final String BOUND_EXPRESSION = "variantExpression";</tt>. 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 <tt>html/style.css</tt> in the plugin <tt>org.eventb.ui</tt>.
| |
− |
| |
− | Here is the result you should get :
| |
− |
| |
− | [[Image:Extend_Rodin_Tuto_1_12_PrettyPrint_for_BoundElement.png|400px]]
| |
− |
| |
− | {{Navigation|Previous= [[Extending_the_Rodin_Event-B_Explorer_(How_to_extend_Rodin_Tutorial)]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= }}
| |
− |
| |
− | [[Category:Developer documentation|*Index]]
| |
− | [[Category:Rodin Platform|*Index]]
| |
− | [[Category:Tutorial|*Index]]
| |