Introduction (How to extend Rodin Tutorial) - Revision history

imported>Tommy: /* Extension Points provided by Eclipse */

2010-10-16T17:03:52Z

Extension Points provided by Eclipse

← Older revision		Revision as of 17:03, 16 October 2010
Line 28:		Line 28:
	Some other extension points are useful to contribute to the GUI:		Some other extension points are useful to contribute to the GUI:
	* <tt>org.eclipse.ui.preferencePages</tt>, which allows to define preference pages (See [http://www.eclipse.org/articles/Article-Preferences/preferences.htm Preferences in the Eclipse Workbench UI]).		* <tt>org.eclipse.ui.preferencePages</tt>, which allows to define preference pages (See [http://www.eclipse.org/articles/Article-Preferences/preferences.htm Preferences in the Eclipse Workbench UI]).
	* <tt>org.eclipse.ui.navigator.navigatorContent</tt> and <tt>org.eclipse.ui.navigator.viewer</tt>, which allows to get a basic navigator to appear with custom content. This extension point will be ~~presented~~ in details in ~~'''//FIXME ajouter ref ici'''~~.		* <tt>org.eclipse.ui.navigator.navigatorContent</tt> and <tt>org.eclipse.ui.navigator.viewer</tt>, which allows to get a basic navigator to appear with custom content. This extension point will be used in details in the section "[[Extending the Rodin Event-B Explorer (How to extend Rodin Tutorial) \| Extending the Rodin Event-B Explorer]]" of this tutorial.

	Finally, a plug-in may contribute help files by using the <tt>org.eclipse.help.toc</tt> extension point. These files may be written by hand or automatically generated from Wiki pages, as explained [[Providing_help_for_your_plug-in_(How_to_extend_Rodin_Tutorial) \| here]].		Finally, a plug-in may contribute help files by using the <tt>org.eclipse.help.toc</tt> extension point. These files may be written by hand or automatically generated from Wiki pages, as explained [[Providing_help_for_your_plug-in_(How_to_extend_Rodin_Tutorial) \| here]].

imported>Tommy: /* Explanations and Outline */

2010-10-16T16:55:58Z

Explanations and Outline

← Older revision		Revision as of 16:55, 16 October 2010
Line 36:		Line 36:

	It is mainly based on one concrete example of step-by-step plug-in development. This example will add Probabilistic Termination and Qualitative Reasoning in Rodin. For more informations about the Probabilistic Termination and Qualitative Reasoning, please refer to the paper of ''Emre Yilmaz and Thai Son Hoang : Development of Rabin's Choice Coordination Algorithm in Event-B in Proceedings of the 10th International Workshop on Automated Verification of Critical Systems (AVoCS 2010)''<br>		It is mainly based on one concrete example of step-by-step plug-in development. This example will add Probabilistic Termination and Qualitative Reasoning in Rodin. For more informations about the Probabilistic Termination and Qualitative Reasoning, please refer to the paper of ''Emre Yilmaz and Thai Son Hoang : Development of Rabin's Choice Coordination Algorithm in Event-B in Proceedings of the 10th International Workshop on Automated Verification of Critical Systems (AVoCS 2010)''<br>
	~~'''//FIXME''' Include link to~~ the paper here		See the corresponding paper here : http://e-collection.ethbib.ethz.ch/eserv/eth:1677/eth-1677-01.pdf

	Other small examples are used in parallel to review all extensions abilities.		Other small examples are used in parallel to review all extensions abilities.

imported>Pascal: /* Extension Points Provided by Eclipse */

2010-09-01T16:48:55Z

Extension Points Provided by Eclipse

← Older revision		Revision as of 16:48, 1 September 2010
Line 17:		Line 17:
	For more information about extension points, please refer to this article: [http://www.eclipse.org/resources/resource.php?id=383 Getting started with Eclipse plug-ins: understanding extension points]. Reading this tutorial implies that you have basic knowledge about eclipse extension mechanism, and programming in Java.		For more information about extension points, please refer to this article: [http://www.eclipse.org/resources/resource.php?id=383 Getting started with Eclipse plug-ins: understanding extension points]. Reading this tutorial implies that you have basic knowledge about eclipse extension mechanism, and programming in Java.

	== Extension Points ~~Provided~~ by Eclipse ==		== Extension Points provided by Eclipse ==
	Eclipse defines extension points that allow plug-ins to contribute behaviours to existing views and editors or to provide implementations for new views and editors (See [http://help.eclipse.org/help33/index.jsp?topic=/org.eclipse.platform.doc.isv/reference/extension-points/org_eclipse_ui_actionSets.html Basic workbench extension points using actions]):		Eclipse defines extension points that allow plug-ins to contribute behaviours to existing views and editors or to provide implementations for new views and editors (See [http://help.eclipse.org/help33/index.jsp?topic=/org.eclipse.platform.doc.isv/reference/extension-points/org_eclipse_ui_actionSets.html Basic workbench extension points using actions]):
	* <tt>org.eclipse.ui.views</tt>		* <tt>org.eclipse.ui.views</tt>

imported>Pascal: /* Explanations and Outline */

2010-09-01T16:47:58Z

Explanations and Outline

← Older revision		Revision as of 16:47, 1 September 2010
Line 33:		Line 33:

	== Explanations and Outline ==		== Explanations and Outline ==
	This tutorial is '''problem solving oriented'''. Hence, all contributions to the platform via plug-in additions will address needs implied by the issues we aim to solve, or functionalities we want to add.~~<br>~~		This tutorial is '''problem solving oriented'''. Hence, all contributions to the platform via plug-in additions will address needs implied by the issues we aim to solve, or functionalities we want to add.

	It is mainly based on one concrete example of step-by-step plug-in development. This example will add Probabilistic Termination and Qualitative Reasoning in Rodin. For more informations about the Probabilistic Termination and Qualitative Reasoning, please refer to the paper of ''Emre Yilmaz and Thai Son Hoang : Development of Rabin's Choice Coordination Algorithm in Event-B in Proceedings of the 10th International Workshop on Automated Verification of Critical Systems (AVoCS 2010)''<br>		It is mainly based on one concrete example of step-by-step plug-in development. This example will add Probabilistic Termination and Qualitative Reasoning in Rodin. For more informations about the Probabilistic Termination and Qualitative Reasoning, please refer to the paper of ''Emre Yilmaz and Thai Son Hoang : Development of Rabin's Choice Coordination Algorithm in Event-B in Proceedings of the 10th International Workshop on Automated Verification of Critical Systems (AVoCS 2010)''<br>
	'''//FIXME''' Include link to the paper here		'''//FIXME''' Include link to the paper here
	~~<br>~~
	Other small examples are used in parallel to review all extensions abilities.		Other small examples are used in parallel to review all extensions abilities.

imported>Pascal: /* Explanations and Outline */

2010-09-01T16:46:49Z

Explanations and Outline

@@ Line 38: / Line 38: @@
 <br>
 Other small examples are used in parallel to review all extensions abilities.
 {{Navigation|Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= [[Creating_a_new_plugin_using_eclipse_(How_to_extend_Rodin_Tutorial)|Creating our plug-in]]}}

imported>Pascal: /* Explanations and Outline */

2010-08-25T12:32:38Z

Explanations and Outline

← Older revision		Revision as of 12:32, 25 August 2010
Line 34:		Line 34:
	== Explanations and Outline ==		== Explanations and Outline ==
	This tutorial is '''problem solving oriented'''. Hence, all contributions to the platform via plug-in additions will address needs implied by the issues we aim to solve, or functionalities we want to add.<br>		This tutorial is '''problem solving oriented'''. Hence, all contributions to the platform via plug-in additions will address needs implied by the issues we aim to solve, or functionalities we want to add.<br>
	~~We will, in a first time, focus~~ on one concrete example of step-by-step plug-in development . This ~~first~~ example will add Probabilistic Termination and Qualitative Reasoning in Rodin. For more informations about the Probabilistic Termination and Qualitative Reasoning, please refer to the paper of ''Emre Yilmaz and Thai Son Hoang : Development of Rabin's Choice Coordination Algorithm in Event-B in Proceedings of the 10th International Workshop on Automated Verification of Critical Systems (AVoCS 2010)''<br>		It is mainly based on one concrete example of step-by-step plug-in development. This example will add Probabilistic Termination and Qualitative Reasoning in Rodin. For more informations about the Probabilistic Termination and Qualitative Reasoning, please refer to the paper of ''Emre Yilmaz and Thai Son Hoang : Development of Rabin's Choice Coordination Algorithm in Event-B in Proceedings of the 10th International Workshop on Automated Verification of Critical Systems (AVoCS 2010)''<br>
	'''//FIXME''' Include link to the paper here		'''//FIXME''' Include link to the paper here
	<br>		<br>
	~~In a second time, we will use~~ small examples, to review all extensions abilities ~~that didn't appear in the first part of this tutorial~~.		Other small examples are used in parallel to review all extensions abilities.

	'''First part''': Extending the UI, through the example of a plug-in for Qualitative Probabilistic Reasoning		'''First part''': Extending the UI, through the example of a plug-in for Qualitative Probabilistic Reasoning

imported>Pascal: /* Explanations and Outline */

2010-08-25T12:29:30Z

Explanations and Outline

← Older revision		Revision as of 12:29, 25 August 2010
Line 39:		Line 39:
	In a second time, we will use small examples, to review all extensions abilities that didn't appear in the first part of this tutorial.		In a second time, we will use small examples, to review all extensions abilities that didn't appear in the first part of this tutorial.

	'''First part''' : ~~extending Rodin with~~ a plug-in for Qualitative Probabilistic Reasoning		'''First part''': Extending the UI, through the example of a plug-in for Qualitative Probabilistic Reasoning
	# [[Creating_a_new_plugin_using_eclipse_(How_to_extend_Rodin_Tutorial)\|Creating our plug-in]]		# [[Creating_a_new_plugin_using_eclipse_(How_to_extend_Rodin_Tutorial)\|Creating our plug-in]]
	# [[Extending_the_Rodin_database_(How_to_extend_Rodin_Tutorial)\|Adding elements to the database (Extending the database)]]		# [[Extending_the_Rodin_database_(How_to_extend_Rodin_Tutorial)\|Adding elements to the database (Extending the database)]]
	# [[Extending_the_Rodin_Structured_Editor_(How_to_extend_Rodin_Tutorial)\|Adding elements in the Rodin structured editor (Extending the structured editor)]]		# [[Extending_the_Rodin_Structured_Editor_(How_to_extend_Rodin_Tutorial)\|Adding elements in the Rodin structured editor (Extending the structured editor)]]
	# [[Extending_the_Rodin_Event-B_Explorer_(How_to_extend_Rodin_Tutorial)\|Adding elements to the Event-B explorer (Extending the navigator)]]		# [[Extending_the_Rodin_Event-B_Explorer_(How_to_extend_Rodin_Tutorial)\|Adding elements to the Event-B explorer (Extending the navigator)]]
	# ~~//extend~~ the ui		# [[Extending_the_Rodin_Pretty Print Page_(How_to_extend_Rodin_Tutorial)\|Displaying elements in the Pretty Print Page (Extending the pretty printer)]]
	~~# //extend~~ the ~~static checker~~
	~~# //extend the proof obligation generator~~
	# [[Providing_help_for_your_plug-in_(How_to_extend_Rodin_Tutorial)\|Documenting your plug-in (Providing Eclipse Help contents)]]		# [[Providing_help_for_your_plug-in_(How_to_extend_Rodin_Tutorial)\|Documenting your plug-in (Providing Eclipse Help contents)]]
	'''Second part''' : ~~extending Rodin (other~~ extension abilities ~~not mentioned above)~~
	#		'''Second part''': Other extension abilities
	#		# //extending the static checker
	#		# //extending the proof obligation generator
	#		# //Adding new reasoners

	{{Navigation\|Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]] \| Next= [[Creating_a_new_plugin_using_eclipse_(How_to_extend_Rodin_Tutorial)\|Creating our plug-in]]}}		{{Navigation\|Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]] \| Next= [[Creating_a_new_plugin_using_eclipse_(How_to_extend_Rodin_Tutorial)\|Creating our plug-in]]}}

imported>Pascal: /* Requirements */

2010-08-23T17:14:38Z

Requirements

← Older revision		Revision as of 17:14, 23 August 2010
Line 53:		Line 53:
	#		#
	#		#

	~~==Requirements==~~

	~~Reading this tutorial implies that you have basic knowledge about eclipse extension mechanism, and programming in Java.<br>~~
	~~For informations about extension points, please refer to this article : [[http://www.eclipse.org/resources/resource.php?id=383]].~~

	~~Moreover, a development environment is required to develop the plug-in code described in this tutorial.<br>~~
	~~'''//FIXME''' Document more about the needed environment to develop plug-ins for Rodin~~

	{{Navigation\|Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]] \| Next= [[Creating_a_new_plugin_using_eclipse_(How_to_extend_Rodin_Tutorial)\|Creating our plug-in]]}}		{{Navigation\|Up= [[Plug-in_Tutorial\|How to extend Rodin Tutorial (Index)]] \| Next= [[Creating_a_new_plugin_using_eclipse_(How_to_extend_Rodin_Tutorial)\|Creating our plug-in]]}}

imported>Pascal: /* Extension Points and Extensions */

2010-08-23T17:14:05Z

Extension Points and Extensions

← Older revision		Revision as of 17:14, 23 August 2010
Line 15:		Line 15:
	In this tutorial, we will define new callers and use the contracts offered by the Rodin platform.		In this tutorial, we will define new callers and use the contracts offered by the Rodin platform.

	For more information about extension points, please refer to this article: [http://www.eclipse.org/resources/resource.php?id=383 Getting started with Eclipse plug-ins: understanding extension points].		For more information about extension points, please refer to this article: [http://www.eclipse.org/resources/resource.php?id=383 Getting started with Eclipse plug-ins: understanding extension points]. Reading this tutorial implies that you have basic knowledge about eclipse extension mechanism, and programming in Java.

	== Extension Points Provided by Eclipse ==		== Extension Points Provided by Eclipse ==

imported>Pascal: /* Explanations and Outline */

2010-08-23T14:53:13Z

Explanations and Outline

← Older revision		Revision as of 14:53, 23 August 2010
Line 47:		Line 47:
	# //extend the static checker		# //extend the static checker
	# //extend the proof obligation generator		# //extend the proof obligation generator
	# [[Providing_help_for_your_plug-in_(How_to_extend_Rodin_Tutorial)\|Documenting your plug-in ~~using~~ Eclipse Help ~~(Providing help~~)]]		# [[Providing_help_for_your_plug-in_(How_to_extend_Rodin_Tutorial)\|Documenting your plug-in (Providing Eclipse Help contents)]]
	'''Second part''' : extending Rodin (other extension abilities not mentioned above)		'''Second part''' : extending Rodin (other extension abilities not mentioned above)
	#		#