Extending the Pretty Print Page - Revision history

imported>Ladenberger at 09:53, 27 October 2011

2011-10-27T09:53:27Z

← Older revision		Revision as of 09:53, 27 October 2011
Line 1:		Line 1:
	{{TOCright}}		{{TOCright}}
	The Pretty 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.		The Pretty Print Page of the [http://handbook.event-b.org/current/html/eventb_editor.html Event-B Editor] provides a rendered view of an edited machine or context, for an quicker and easier reading.

	[[Image:PrettyPrintPage.png\|480px\|center\|An example of pretty print page]]		[[Image:PrettyPrintPage.png\|480px\|center\|An example of pretty print page]]

imported>Pascal: /* Category */

2010-05-04T07:50:22Z

imported>Tommy at 10:08, 16 April 2010

2010-04-16T10:08:07Z

@@ Line 24: / Line 24: @@
 * <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>.
+: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>.(see [[#Display implicit children]])
 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.
@@ Line 242: / Line 242: @@
 [[Image:ExtendedConvergence.png]]
 ----

imported>Tommy at 09:23, 16 April 2010

2010-04-16T09:23:33Z

imported>Tommy at 08:58, 16 April 2010

2010-04-16T08:58:46Z

← Older revision		Revision as of 08:58, 16 April 2010
Line 190:		Line 190:
	====Example of events pretty printer====		====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).		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).

			[[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.		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.
Line 236:		Line 238:
	*<tt>decrementLevel()</tt> : decrements 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 display below for a sample refinement :

			[[Image:ExtendedConvergence.png]]
	----		----

imported>Tommy at 08:52, 16 April 2010

2010-04-16T08:52:31Z

@@ Line 45: / Line 45: @@
       for each Element e in parent.elementsOfType(c)
       do
          '''IElementPrettyPrinter p = e.getPrettyPrinter();'''
          '''p.prettyPrint(e, parent);'''
          //recursive traverse to continue pretty printing child elements
          ''traverse(e);''
-         appendItemEnding(e);
+         p.appendItemEnding(e); // Used to print attributes or additional info
       od
     od
@@ Line 76: / Line 76: @@
 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.
+::(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.
+::(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>
 == How to implement pretty printers (of Event-B Editor contributions) ==
@@ Line 94: / Line 96: @@
 * 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.
@@ Line 140: / Line 142: @@
 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===
@@ Line 170: / Line 172: @@
 This method implement a specific behavior 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===
 This section explains how to append attribute or any other information to the HTML stream.

imported>Tommy: /* Append element attributes or details */

2010-04-15T18:03:05Z

Append element attributes or details

← Older revision		Revision as of 18:03, 15 April 2010
Line 172:		Line 172:

	===Append element attributes or details===		===Append element attributes or details===

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

imported>Tommy at 17:59, 15 April 2010

2010-04-15T17:59:56Z

← Older revision		Revision as of 17:59, 15 April 2010
Line 141:		Line 141:
	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.		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.

	===~~Redefining~~ the contributed prefix===		===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.		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.

imported>Tommy: /* Redefining the contributed prefix */

2010-04-15T17:59:12Z

Redefining the contributed prefix

← Older revision		Revision as of 17:59, 15 April 2010
Line 163:		Line 163:
	}		}
	} catch (RodinDBException e) {		} catch (RodinDBException e) {
	EventBEditorUtils.debugAndLogError(e, "Cannot get all guards of "+ parent.getElementName());		EventBEditorUtils.debugAndLogError(e, "Cannot get all guards of " + parent.getElementName());
	}		}
	return true;		return true;
	}		}

			This method implement a specific behavior 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===		===Append element attributes or details===

imported>Tommy: /* Redefining the contributed prefix */

2010-04-15T17:38:27Z

Redefining the contributed prefix

← Older revision		Revision as of 17:38, 15 April 2010
Line 142:		Line 142:

	===Redefining the contributed prefix===		===Redefining 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;
			}

	===Append element attributes or details===		===Append element attributes or details===

← Older revision		Revision as of 07:50, 4 May 2010
Line 1:		Line 1:
	{{TOCright}}		{{TOCright}}
	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.		The Pretty 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.

	[[Image:PrettyPrintPage.png\|480px\|center\|An example of pretty print page]]		[[Image:PrettyPrintPage.png\|480px\|center\|An example of pretty print page]]
Line 262:		Line 262:

	where the CSS classes for implicit guards let them (the guard label and the guard predicate) be displayed in italic.		where the CSS classes for implicit guards let them (the guard label and the guard predicate) be displayed in italic.

			[[Category:Developer documentation]]

← Older revision		Revision as of 09:23, 16 April 2010
Line 66:		Line 66:
	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.		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 :		'''''There are 4 methods one can implement defining a pretty printer for an element :'''''

	<tt>		<tt>
Line 105:		Line 105:
	The display wanted is described by the picture above, and the corresponding implementation is the following :		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 ~~editorItem~~ contribution for variables, 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>		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 {..}		public class VariablesPrettyPrinter extends DefaultPrettyPrinter implements IElementPrettyPrinter {..}
	and override only the <tt>prettyPrint</tt> method which is the following :		and override only the <tt>prettyPrint</tt> method which is the following :
Line 134:		Line 134:
	}		}

	We can see here that the HTML is ~~build~~ with the <tt>IPrettyPrintStream</tt> method <tt>appendString()</tt> and that we retrieve the CSS class for variables by defining a constant		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";		private static final String VARIABLE_IDENTIFIER = "variableIdentifier";

	and using the methods <tt>getHTMLBeginForCSSClass()</tt> and <tt>getHTMLEndForCSSClass()</tt> to retrieve the HTML/CSS code		and using the methods <tt>getHTMLBeginForCSSClass()</tt> and <tt>getHTMLEndForCSSClass()</tt> to retrieve the HTML/CSS code
	as the class is defined in the style.css file by :		as the class is defined in the <tt>style.css</tt> file by :
	.variableIdentifier {font-size:16px; color:black;font-family:"Brave Sans Mono";}		.variableIdentifier {font-size:16px; color:black;font-family:"Brave Sans Mono";}

Line 170:		Line 170:
	}		}

	This method ~~implement~~ a specific ~~behavior~~ and prints the keyword WHEN as if the core pretty printer did, using the method <tt>appendKeyword()</tt> from IPrettyPrintStream.		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.		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.
	----		----
Line 238:		Line 238:
	*<tt>decrementLevel()</tt> : decrements 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 display ~~below~~ for a sample refinement :		We finally obtain the following display, here for the initialisation of a sample refinement :

	[[Image:ExtendedConvergence.png]]		[[Image:ExtendedConvergence.png]]
	----		----