Single View Design - Revision history

imported>Jrloria: /* Statistics */

2010-03-26T18:35:45Z

Statistics

← Older revision		Revision as of 18:35, 26 March 2010
Line 65:		Line 65:

	It is possible to select multiple elements in the navigator and get a combined statistics. But the selected elements must be on the same level (e.g. projects, machines/contexts). This mean if you select both machines and projects at the same time, you won't get any statistics.		It is possible to select multiple elements in the navigator and get a combined statistics. But the selected elements must be on the same level (e.g. projects, machines/contexts). This mean if you select both machines and projects at the same time, you won't get any statistics.

			===See Also===
			* [[Extending Single View Design]]

	[[Category:User documentation]]		[[Category:User documentation]]
	[[Category:Design]]		[[Category:Design]]

imported>Jrloria at 18:31, 26 March 2010

2010-03-26T18:31:43Z

← Older revision		Revision as of 18:31, 26 March 2010
Line 66:		Line 66:
	It is possible to select multiple elements in the navigator and get a combined statistics. But the selected elements must be on the same level (e.g. projects, machines/contexts). This mean if you select both machines and projects at the same time, you won't get any statistics.		It is possible to select multiple elements in the navigator and get a combined statistics. But the selected elements must be on the same level (e.g. projects, machines/contexts). This mean if you select both machines and projects at the same time, you won't get any statistics.

	[[Category:~~Developer~~ documentation]]		[[Category:User documentation]]
	[[Category:Design]]		[[Category:Design]]

imported>Jrloria: /* Developer guide */ moved to Extending Single View Design

2010-03-26T18:29:46Z

Developer guide: moved to Extending Single View Design

@@ Line 66: / Line 66: @@
 It is possible to select multiple elements in the navigator and get a combined statistics. But the selected elements must be on the same level (e.g. projects, machines/contexts). This mean if you select both machines and projects at the same time, you won't get any statistics.
 [[Category:Developer documentation]]
 [[Category:Design]]

imported>Nicolas: /* Content */ Terminology change: theorem -> derived invariant

2009-05-19T09:39:06Z

Content: Terminology change: theorem -> derived invariant

← Older revision		Revision as of 09:39, 19 May 2009
Line 42:		Line 42:
	*'''Invariants'''		*'''Invariants'''
	*'''Events'''		*'''Events'''
	*'''Proof Obligations''': All proof obligations of a machine, context, axiom, invariant, ~~theorem~~ or event.		*'''Proof Obligations''': All proof obligations of a machine, context, axiom, invariant, derived invariant or event.

	Here is an example of what the same project looks like when using the complex machine and context structure (left) and when using the simple version (right).		Here is an example of what the same project looks like when using the complex machine and context structure (left) and when using the simple version (right).

imported>Nicolas: /* Content */ No more theorems in view customization, subsequently to "Theorems everywhere".

2009-05-14T12:24:19Z

Content: No more theorems in view customization, subsequently to "Theorems everywhere".

← Older revision		Revision as of 12:24, 14 May 2009
Line 41:		Line 41:
	*'''Axioms'''		*'''Axioms'''
	*'''Invariants'''		*'''Invariants'''
	*'''Theorems'''
	*'''Events'''		*'''Events'''
	*'''Proof Obligations''': All proof obligations of a machine, context, axiom, invariant, theorem or event.		*'''Proof Obligations''': All proof obligations of a machine, context, axiom, invariant, theorem or event.

imported>Mathieu: CVS -> SVN

2009-03-31T11:55:51Z

CVS -> SVN

← Older revision		Revision as of 11:55, 31 March 2009
Line 76:		Line 76:

	====Adding a content provider to the navigator====		====Adding a content provider to the navigator====
	To add a custom content provider you have to use the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new navigatorContent. Example: You want to add a new child under the IMachineRoot nodes. Define a navigatorContent and add triggerPoints. There you add a new <code>instanceof</code> with value <code>org.eventb.core.IMachineRoot </code>. The priority of the navigatorContent decides in what order the content is shown with respect to other content providers. (For example the content provider for the variables has a higher priority than the one for invariants, that's why the variables appear before the invariants in the tree.) You need to provide a contentProvider and a labelProvider class. Finally include your navigatorContent in your viewerContentBindings. For more information read the extension point description of [http://help.eclipse.org/help32/index.jsp?topic=/org.eclipse.platform.doc.isv/reference/extension-points/org_eclipse_ui_navigator_navigatorContent.html navigatorContent]. There is a example project in the ~~CVS~~ repository, that adds a content provider to the navigator.		To add a custom content provider you have to use the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new navigatorContent. Example: You want to add a new child under the IMachineRoot nodes. Define a navigatorContent and add triggerPoints. There you add a new <code>instanceof</code> with value <code>org.eventb.core.IMachineRoot </code>. The priority of the navigatorContent decides in what order the content is shown with respect to other content providers. (For example the content provider for the variables has a higher priority than the one for invariants, that's why the variables appear before the invariants in the tree.) You need to provide a contentProvider and a labelProvider class. Finally include your navigatorContent in your viewerContentBindings. For more information read the extension point description of [http://help.eclipse.org/help32/index.jsp?topic=/org.eclipse.platform.doc.isv/reference/extension-points/org_eclipse_ui_navigator_navigatorContent.html navigatorContent]. There is a example project in the SVN repository, that adds a content provider to the navigator.

	<code>		<code>
Line 110:		Line 110:

	====Adding a filter to the navigator====		====Adding a filter to the navigator====
	To add a custom filter you have to use the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new commonFilter. You can either provide an implementation for <code>ViewerFilter</code> or use xml filterExpressions. For more information read the extension point description of [http://help.eclipse.org/help32/index.jsp?topic=/org.eclipse.platform.doc.isv/reference/extension-points/org_eclipse_ui_navigator_navigatorContent.html navigatorContent]. Finally include your commonFilter in your viewerContentBindings. There is a example project in the ~~CVS~~ repository, that adds a filter to the navigator.		To add a custom filter you have to use the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new commonFilter. You can either provide an implementation for <code>ViewerFilter</code> or use xml filterExpressions. For more information read the extension point description of [http://help.eclipse.org/help32/index.jsp?topic=/org.eclipse.platform.doc.isv/reference/extension-points/org_eclipse_ui_navigator_navigatorContent.html navigatorContent]. Finally include your commonFilter in your viewerContentBindings. There is a example project in the SVN repository, that adds a filter to the navigator.

	====Adding an action provider to the navigator====		====Adding an action provider to the navigator====
	To add a custom filter you use again the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new actionProvider. You have to provide an implementation for <code>org.eclipse.ui.navigator.CommonActionProvider</code>. To decide on what nodes in the tree your action provider should be invoked, use the enablement expression. Finally include your commonFilter in your viewerActionBindings. There is a example project in the ~~CVS~~ repository, that adds an action provider to the navigator.		To add a custom filter you use again the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new actionProvider. You have to provide an implementation for <code>org.eclipse.ui.navigator.CommonActionProvider</code>. To decide on what nodes in the tree your action provider should be invoked, use the enablement expression. Finally include your commonFilter in your viewerActionBindings. There is a example project in the SVN repository, that adds an action provider to the navigator.

	[[Category:User documentation]]		[[Category:User documentation]]
	[[Category:Developer documentation]]		[[Category:Developer documentation]]
	[[Category:Design]]		[[Category:Design]]

imported>Mathieu: Category:User documentation Category:Developer documentation Category:Design

2009-03-04T09:26:32Z

Category:User documentation Category:Developer documentation Category:Design

← Older revision		Revision as of 09:26, 4 March 2009
Line 115:		Line 115:
	To add a custom filter you use again the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new actionProvider. You have to provide an implementation for <code>org.eclipse.ui.navigator.CommonActionProvider</code>. To decide on what nodes in the tree your action provider should be invoked, use the enablement expression. Finally include your commonFilter in your viewerActionBindings. There is a example project in the CVS repository, that adds an action provider to the navigator.		To add a custom filter you use again the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new actionProvider. You have to provide an implementation for <code>org.eclipse.ui.navigator.CommonActionProvider</code>. To decide on what nodes in the tree your action provider should be invoked, use the enablement expression. Finally include your commonFilter in your viewerActionBindings. There is a example project in the CVS repository, that adds an action provider to the navigator.

	[[Category:~~Work in progress~~]]		[[Category:User documentation]]
			[[Category:Developer documentation]]
			[[Category:Design]]

imported>Laurent: /* Content */

2009-01-29T13:17:13Z

Content

← Older revision		Revision as of 13:17, 29 January 2009
Line 45:		Line 45:
	*'''Proof Obligations''': All proof obligations of a machine, context, axiom, invariant, theorem or event.		*'''Proof Obligations''': All proof obligations of a machine, context, axiom, invariant, theorem or event.

	Here's an example of what the same ~~projects~~ looks like ~~once~~ using the complex machine and context structure (left) and ~~once~~ using the simple version (right).		Here is an example of what the same project looks like when using the complex machine and context structure (left) and when using the simple version (right).

	[[Image:Complex.jpg]][[Image:Simple.jpg]]		[[Image:Complex.jpg]][[Image:Simple.jpg]]

imported>Laurent: /* Specification */

2009-01-29T13:16:00Z

Specification

← Older revision		Revision as of 13:16, 29 January 2009
Line 15:		Line 15:

	===The Navigator===		===The Navigator===
	The navigator contains a tree of all projects and their contents. The users can choose between to ways how the machines and contexts will be presented:		The navigator contains a tree of all projects and their contents. The users can choose between two ways how the machines and contexts will be presented:
	*A simple structure where all machines and contexts are presented on the same level		*A simple structure where all machines and contexts are presented on the same level
	*A complex structure where the machines and contexts are presented as a tree. Thus dependencies between machines and contexts (like ''refines'' or ''sees'') are made visible.		*A complex structure where the machines and contexts are presented as a tree. Thus dependencies between machines and contexts (like ''refines'' or ''sees'') are made visible.

imported>Laurent: /* Purpose */

2009-01-29T13:12:15Z

Purpose

← Older revision		Revision as of 13:12, 29 January 2009
Line 5:		Line 5:
	* The ''Obligation Explorer'' displays the proof obligations together with their proof state.		* The ''Obligation Explorer'' displays the proof obligations together with their proof state.

	The clean separation between modelling and proving looked good during paper design. However, users reported that they were constantly switching between the two views. This is due to the fact that modelling and proving are not ~~separated~~ activities, one performed after the other. In general practice, both activities are intertwined.		The clean separation between modelling and proving looked good during paper design. However, users reported that they were constantly switching between the two views. This is due to the fact that modelling and proving are not separate activities, one being performed after the other. In general practice, both activities are intertwined.

	Independently, Eclipse has released a new framework called the ''Common Navigation Framework'' since these two views were designed and implemented. The purpose of this framework is ~~two~~ provide Eclipse plug-ins with basic blocks for implementing views like the ''Project Explorer''.		Independently, Eclipse has released a new framework called the ''Common Navigation Framework'' since these two views were designed and implemented. The purpose of this framework is to provide Eclipse plug-ins with basic blocks for easily implementing views like the ''Project Explorer''. Moreover, this framework allows various plug-ins to cooperate together in populating such views, thus reinforcing plug-in integration into the platform.

	Therefore, it was decided in the Deploy project to combine the two original views ~~with~~ a single one that would display ~~both~~ modelling elements and proof obligations together. This new single view should also take advantage of the ''Common Navigation Framework'', in order to improve its seamless integration within Eclipse.		Therefore, it was decided in the Deploy project to combine the two original views into a single one that would display modelling elements and proof obligations together. This new single view should also take advantage of the ''Common Navigation Framework'', in order to improve its seamless integration within Eclipse.

	==Specification==		==Specification==