Difference between pages "Rodin Developer Support" and "Rodin Editor"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Renato
 
imported>Tommy
 
Line 1: Line 1:
−
The Developer Support provides resources for developing plug-ins for the Rodin Platform.
+
{{TOCright}}
 +
Return to [[Rodin Plug-ins]]
  
 +
[[Image:RodinEditor_basicView1.png|400px|left|a basic view of the Rodin Editor on a context]]
  
−
== Rodin Platform Overview ==
+
The Rodin Editor is an editor, based on the same principles as the historical structured Event-B Editor. This latter editor shown its weakness while editing large models. Moreover, it was impossible to show some information, which are needed when one edits an Event-B model (such as the inherited elements which were formerly displayed only in the pretty print view). This is to solve all these issues that the Rodin Editor was created.
−
see [[How To Contribute]]
 
  
−
== Architecture of the Rodin Platform ==
+
This editor aims to be clean, in order to read easily models, but new comers may find it less easy to use. Please read the '''Principles''' section to get the necessary background to understand how this editor works. Furthermore, the text base of this editor aims to bring with it all the navigation and edition ease provided by text editor.
 +
<br style="clear: both" />
  
−
=== Rodin Platform Core ===
+
=== Installation Details ===
 +
{{TODO}} Document this part when the plug-in is released.
  
−
* [[Database]]
+
=== Principles ===
 +
'''The component contents are displayed as text.''' Once you component opened with the Rodin Editor, its contents are printed as text inside the Rodin Editor. However, as said, the Rodin Editor is not a text editor, and even if the component you edit is streamlined to basic text, what you edit is stored in an underlying database. That's the reason why you can not type text at any place at any moment. (i.e. there is no parsing of text file: what you see is a text component based form editor).
  
−
* [[Builder]]
+
'''There are two types of edition possible.''' Because Rodin manipulates Event-B elements and their attributes, the Rodin Editor provides two ways to modify Event-B models:
 +
* you can navigate through the model contents and do things on the Event-B elements (e.g. add/remove/move/etc.) with the right-click actions or the keyboard shortcuts, depending on where is your cursor, or what you selected,
 +
* you can edit the Event-B element's attributes by entering the "edition" mode provided by the overlay editor. This is detailed here-after.
  
−
* [[Rodin Index Design]]
+
'''An overlay editor displays over the text to edit element's attributes''' The basic idea is: ''"when I want to edit some contents, I should open the overlay editor that will allow me to modify its value"''.
  
−
* [[Indexing System]]
+
'''Everything happens where I click, or where my text caret is.''' The caret position, also set when the user left-clicks in the editor, is the base for component modifications:
 +
* if you click an editable attribute, the overlay editor opens on it and you are able to modify the attribute. The same action is possible if you press "Backspace" if the caret is on an editable attribute,
 +
* if you click on non editable places of the editor, you just move the text caret to the pointed position.
  
−
* [[Undo Redo]]
+
=== A basic edition exemple ===
 +
The Rodin Editor might not be the 'preferred' editor that Rodin uses to open your Event-B models.<br>
 +
Thus, to open a component (e.g. a machine, a context, etc.), '''right-click''' on it and select '''Open with''' > '''Rodin Editor'''.
 +
The context component is then opened with the Rodin Editor.
  
−
* [[File Root Separation]]
+
=== Available keyboard shortcurts ===
 +
Here is the list of the currently key bindings which are set by default and specific to the Rodin Editor.
  
−
=== Event-B User Interface ===
+
{{SimpleHeader}}
 +
|-
 +
! scope=col | KEY SEQUENCE || ACTION
 +
|-
 +
| BACKSPACE (ENTER) || Enter the edition mode using the overlay editor if the caret is on an editable place.
 +
|-
 +
| DEL || Suppress the element after the caret position
 +
|-
 +
| CTRL+T || Add a sibling of the element pointed by the caret position. The sibling is placed just after this latter one.
 +
|-
 +
| CTRL+SHIFT+N || Opens a popup to select the element type of the child to add to the element pointed by the caret position. Note that if there is only one child type, the child will be directly created.
 +
|-
 +
| CTRL+BACKSPACE || Insert a new carriage return while editing with the overlay editor.
 +
|-
 +
| ALT+ARROW_UP || Move up the selected elements.
 +
|-
 +
| ALT+ARROW_DOWN || Move down the selected elements.
 +
|-
 +
| SHIFT+ARROW_UP || Select elements up.
 +
|-
 +
| SHIFT+ARROW_DOWN || Select elements down.
 +
|-
 +
| ALT+ESC || Quit the current overlay edition (if any) and forget the modifications made, frees the current selection.
 +
|-
 +
| TAB || Go to the next editable place (i.e. to the next editable element attribute)
 +
|-
 +
| SHIFT+TAB || Go to the previous editable place (i.e. to the next editable element attribute)
 +
|}
  
−
The Event-B User Interface of the Roding Platform has two major components that are concerned with either [[Modelling User Interface|modelling]] in Event-B or [[Proving User Interface|proving]] properties of models.
+
==== Customize this list ====
 +
If you don't like these shortcuts, you can modify them by setting your own key preferences.
 +
To do so, go to Window > Preferences and then General > Key. A table appears were you can find and edit the shortcuts.
  
−
* [[Modelling User Interface]]
+
==== Tips & Tricks ====
 +
A command currently (i.e. in Rodin 2.2) disable the possibility to use the ESC instead of ALT+ESC sequence. This is quite cumbersome, and can be tuned!
 +
To do so, open the preference table for key shortcuts (described above) and after ensuring you disabled the filters of uncategorized commands (using the Filters... dialog)
 +
search for the command named "Restore Styles". This is the command to release the highlights in the proving views. You can then swith the sequence of this command to ALT+ESC and change the value of the "Abort edition and free selected items" command to ESC. After applying these settings, the shortcuts will be modified as wished above.
  
−
* [[Proving User Interface]]
+
[[Category:Plugin]]
−
 
+
[[Category:User documentation]]
−
Apart from these are more minor components.
 
−
 
 
−
* [[Proof Purger Design|Proof Purger]] allows to delete unused proofs.
 
−
 
 
−
* [[Proof Skeleton Design]] is a view that displays skeletons of existing proofs
 
−
 
 
−
* [[Auto-Completion Design]] proposes a list of names to the user editing a model
 
−
 
 
−
=== Event-B Component Library ===
 
−
 
 
−
Event-B models and all proof-related information are stored in the Rodin database. The syntax of the mathematical notation, that is, expressions, predicates, and assignments, are maintained in an [[Abstract Syntax Tree|abstract syntax tree]]. Abstract syntax trees are manipulated by means of a class library that can be used independently of Eclipse. They are saved in the database in human-readable form as Unicode character strings. Event-B constructs, such as contexts and machines, are not represented as abstract syntax trees. They are stored and retrieved directly from the database (by contrast, mathematical formulas need additional parsing). Well-formedness of Event-B constructs is verified by a [[Static Checker|static checker]]. The static checker has two main purposes: (1) it generates error messages for ill-formed constructs, and (2) it filters well-formed parts of components to be subjected to proof obligation generation. The [[Proof Obligation Generator|proof obligation generator]] uses those parts of constructs that are well-formed and generates proof obligations from them. Finally, the [[Proof Manager|proof manager]] attempts to prove proof obligations and maintains existing proofs associated with proof obligations. The proof manager works automatically and interactively. When new proof obligations have been generated it attempts to discharge them automatically. If it does not succeed, it permits interactive proof (by means of the [[Proving User Interface|proving user interface]]).
 
−
 
 
−
* [[Abstract Syntax Tree]]
 
−
 
 
−
* [[Static Checker]]
 
−
 
 
−
* [[Proof Obligation Generator]]
 
−
 
 
−
* [[Proof Manager]]
 
−
 
 
−
* [[Proof Simplification]]
 
−
 
 
−
== Extending Rodin ==
 
−
 
 
−
* [[Getting Started]]
 
−
 
 
−
* [[Plug-in Tutorial]]
 
−
 
 
−
* [[Extending the Rodin Database]]
 
−
 
 
−
* [[Extending the project explorer]]
 
−
 
 
−
* [[Extending the Structure Editor]]
 
−
 
 
−
* [[Extending the Pretty Print Page]]
 
−
 
 
−
* [[Extending the Proof Manager]]
 
−
 
 
−
* [[Extending the Index Manager]]
 
−
 
 
−
* [[Extending the Static Checker]]
 
−
 
 
−
* [[Index Query]]
 
−
 
 
−
== Useful Hints ==
 
−
 
 
−
=== Version Control ===
 
−
 
 
−
All sources of the core Rodin platform (and of some plug-ins) are managed under version control in SourceForge.  The repository currently used is Subversion and can be accessed using URL [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp].
 
−
 
 
−
=== Building against a version of Rodin ===
 
−
 
 
−
To develop extensions to the Rodin platform your code build needs access to a consistent (version-wise) set of Rodin platform plug-ins. (Don't just check out the latest versions from 'Head' because it may be under development and in an inconsistent state). An easy way to set up your workspace is to import the Rodin platform source code from SVN into your workspace using the 'Releng' plug-in. See [http://wiki.event-b.org/index.php/FAQ#Installing_the_sources_from_Subversion_in_Eclipse Installing the sources from Subversion in Eclipse] for further instructions.
 
−
 
 
−
Alternatively, you can set your plugin development target platform to any Rodin installation you have installed (Eclipse-Preferences-Plug-in Development-Target Platform). This is useful as a final test that everything will work once installed into Rodin but because it uses a 'built' platform, you don't get access to the Rodin source code (e.g. for de-bugging).
 
−
 
 
−
=== Testing ===
 
−
 
 
−
=== Debugging ===
 
−
 
 
−
=== Publishing ===
 
−
 
 
−
A Plug-in developed for the Rodin Platform will normally consist of a collection of eclipse 'plugin' projects and a single eclipse 'feature' project. The feature project contains branding information such as logo's icons and licensing details. It is also used to identify your Plug-in so that users can install it. To build your Plug-in use an eclipse 'site' project. This will build the jar files for your plugin projects and a jar for your feature. See eclipse documentation for more details.
 
−
 
 
−
Now you need to make your Plug-in available for users to install via the Main Rodin Update site (which comes built-in to the Rodin platform).
 
−
 
 
−
First upload your jar files onto the Sourceforge uploads area and then create a new release in the FRS (Admin-file releases). Note that you should include a zip of the complete source projects to comply with Sourceforge rules. You must not repeat files that have not changed. Sourceforge does not allow you to upload multiple copies of the same jar file. The Feature jar will take care of unchanged plugin jars and use the existing links. Only new jars should be included in a particular release.
 
−
See here for details:- http://alexandria.wiki.sourceforge.net/File+Release+System+-+Offering+Files+for+Download
 
−
 
 
−
Finally, the update site must be updated to redirect the update requests to the files on the FRS.
 
−
(Currently this is done by Colin Snook on request - see Rodin developers page for contact details).
 
−
 
 
−
[[Details for Maintaining Main Rodin Update Site]]
 
−
 
 
−
== Rodin Developer FAQ ==
 
−
 
 
−
see [[Developer FAQ]].
 
−
 
 
−
[[Category:Developer documentation]]
 
−
[[Category:Rodin Platform]]
 

Revision as of 13:29, 12 July 2011

Return to Rodin Plug-ins

a basic view of the Rodin Editor on a context

The Rodin Editor is an editor, based on the same principles as the historical structured Event-B Editor. This latter editor shown its weakness while editing large models. Moreover, it was impossible to show some information, which are needed when one edits an Event-B model (such as the inherited elements which were formerly displayed only in the pretty print view). This is to solve all these issues that the Rodin Editor was created.

This editor aims to be clean, in order to read easily models, but new comers may find it less easy to use. Please read the Principles section to get the necessary background to understand how this editor works. Furthermore, the text base of this editor aims to bring with it all the navigation and edition ease provided by text editor.

Installation Details

TODO Document this part when the plug-in is released.

Principles

The component contents are displayed as text. Once you component opened with the Rodin Editor, its contents are printed as text inside the Rodin Editor. However, as said, the Rodin Editor is not a text editor, and even if the component you edit is streamlined to basic text, what you edit is stored in an underlying database. That's the reason why you can not type text at any place at any moment. (i.e. there is no parsing of text file: what you see is a text component based form editor).

There are two types of edition possible. Because Rodin manipulates Event-B elements and their attributes, the Rodin Editor provides two ways to modify Event-B models:

  • you can navigate through the model contents and do things on the Event-B elements (e.g. add/remove/move/etc.) with the right-click actions or the keyboard shortcuts, depending on where is your cursor, or what you selected,
  • you can edit the Event-B element's attributes by entering the "edition" mode provided by the overlay editor. This is detailed here-after.

An overlay editor displays over the text to edit element's attributes The basic idea is: "when I want to edit some contents, I should open the overlay editor that will allow me to modify its value".

Everything happens where I click, or where my text caret is. The caret position, also set when the user left-clicks in the editor, is the base for component modifications:

  • if you click an editable attribute, the overlay editor opens on it and you are able to modify the attribute. The same action is possible if you press "Backspace" if the caret is on an editable attribute,
  • if you click on non editable places of the editor, you just move the text caret to the pointed position.

A basic edition exemple

The Rodin Editor might not be the 'preferred' editor that Rodin uses to open your Event-B models.
Thus, to open a component (e.g. a machine, a context, etc.), right-click on it and select Open with > Rodin Editor. The context component is then opened with the Rodin Editor.

Available keyboard shortcurts

Here is the list of the currently key bindings which are set by default and specific to the Rodin Editor.


KEY SEQUENCE ACTION
BACKSPACE (ENTER) Enter the edition mode using the overlay editor if the caret is on an editable place.
DEL Suppress the element after the caret position
CTRL+T Add a sibling of the element pointed by the caret position. The sibling is placed just after this latter one.
CTRL+SHIFT+N Opens a popup to select the element type of the child to add to the element pointed by the caret position. Note that if there is only one child type, the child will be directly created.
CTRL+BACKSPACE Insert a new carriage return while editing with the overlay editor.
ALT+ARROW_UP Move up the selected elements.
ALT+ARROW_DOWN Move down the selected elements.
SHIFT+ARROW_UP Select elements up.
SHIFT+ARROW_DOWN Select elements down.
ALT+ESC Quit the current overlay edition (if any) and forget the modifications made, frees the current selection.
TAB Go to the next editable place (i.e. to the next editable element attribute)
SHIFT+TAB Go to the previous editable place (i.e. to the next editable element attribute)

Customize this list

If you don't like these shortcuts, you can modify them by setting your own key preferences. To do so, go to Window > Preferences and then General > Key. A table appears were you can find and edit the shortcuts.

Tips & Tricks

A command currently (i.e. in Rodin 2.2) disable the possibility to use the ESC instead of ALT+ESC sequence. This is quite cumbersome, and can be tuned! To do so, open the preference table for key shortcuts (described above) and after ensuring you disabled the filters of uncategorized commands (using the Filters... dialog) search for the command named "Restore Styles". This is the command to release the highlights in the proving views. You can then swith the sequence of this command to ALT+ESC and change the value of the "Abort edition and free selected items" command to ESC. After applying these settings, the shortcuts will be modified as wished above.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Rodin_Developer_Support&oldid=7101’