Difference between pages "Rodin Editor" and "Rodin Editor User Guide"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
imported>Tommy
 
Line 1: Line 1:
−
{{TOCright}}
+
== Introduction ==
−
Return to [[Rodin Plug-ins]]
 
  
−
[[Image:RodinEditor_basicView1.png|400px|left|a basic view of the Rodin Editor on a context]]
+
The Rodin Editor plug-in provides a structured editor to model in Event-B withing Rodin. This editor uses a textual representation, and edition is done through an overlay text editor and action depending on the caret position in the text.<br>
 +
For more details about the principles of this editor,  see [[Rodin_Editor|the Rodin Editor Plug-in page]].
 +
''<span style="color:#FF4500">IMPORTANT :  we identified a source of concurrency issue in the current version (0.5.0) of the plug-in.</span>''<br>
 +
<span style="color:#FF4500">'''To avoid any trouble, please do not generate files while having some Rodin Editor open, and edit only one model per project at once.'''</span>
  
−
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.
+
== Installation ==
  
−
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.
+
=== Setup ===
−
<br style="clear: both" />
+
Install the Rodin Editor plug-in:
 +
# In the menu choose Help -> Install New Software...
 +
# In the Work with dropdown list, choose the location URL: Rodin - http://rodin-b-sharp.sourceforge.net/updates
 +
# Select the Rodin Editor feature then click the check box
 +
# Click Next, after some time, the Install Details page appears
 +
# Click Next and accept the license
 +
# Click Finish
 +
# A Security Warning window may appear: click OK
 +
# Restart Rodin as suggested.
 +
Now you are ready to use the new Rodin Editor plug-in.
  
−
Please have a look also at the [[Rodin Editor User Guide]].
+
=== Release Notes ===
−
=== Current version ===
+
See [[Rodin_Editor_Release_History | Rodin Editor Release Notes]]
−
Since Rodin 2.4, release on February 2nd, the Rodin Editor is part of the core platform.
 
  
−
Thus, the Rodin Editor is no longer available as a separate plug-in from the main Rodin update site.
 
  
−
=== Principles ===
+
== Editing ==
−
'''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:
+
This is a small exercice to get used to the principles of the new structured editor. It is based on the 'Celebrity' project of the tutorial. You can download the resulting project [http://sourceforge.net/projects/rodin-b-sharp/files/Doc_%20Tutorial/1.1/Celebrity.zip/download <tt>here</tt>].<br>
−
* 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,
+
We will here build the context ''Celebrity_C0''.
−
* 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"''.
+
=== Create a context, add elements to it ===
 +
Let's create a Rodin project, and add a context component called ''Celebrity_C0'' to it.<br>
 +
-- By opening this context with the Rodin Editor (right click > Open with > Rodin Editor) you shall obtain the following:<br>
 +
[[Image:RodinEditor_UserGuide_step1.png]]
  
−
'''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:
+
This editor allows to do things based on the position of the caret.<br>
−
* 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,
+
-- Place the caret at one location on the line of the context label, and before the label, as on the figure below:
−
* if you click on non editable places of the editor, you just move the text caret to the pointed position.
 
  
−
'''Implicit elements are displayed in grayed colors.''' The elements that are implicit at the current level of edition are not editable, and displayed in grayed colors. (See the figure below)
+
[[Image:RodinEditor_UserGuide_step2.png]]
−
[[Image:RodinEditor_basicView4.png|500px|center]]
 
  
−
=== A basic overview ===
+
-- Then right click, and add a 'Constant' child using the menus :
−
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'''.<br>
 
−
The context component is then opened with the Rodin Editor.<br>
 
  
−
[[Image:RodinEditor_basicView2.png|600px]]
+
[[Image:RodinEditor_UserGuide_step3.png|600px]]
  
−
On the figure above, you see the context component.<br>
+
-- Save the file. <br>
−
* The user is editing the axiom ''axm8'' and we see that the text is black and the background is grayed. This is the actually the overlay editor, that is open to edit the predicate contained by the axiom ''axm8''.
+
After saving the file, the error markers are recalculated, and you have an error that appears on the newly created constant 'cst1'.<br>
−
* There are buttons in the left ruler to fold some elements.
+
You shall see this :
−
* The comments are preceeded by the character ' › ' to indicate where to click for edition.
 
−
* The other attributes are inlined as grayed text.
 
−
** Note that : some attributes have type boolean, thus change value on click, and some attributes are choice attributes thus display a list of clickable values (see the image below) on click.
 
  
−
[[Image:RodinEditor_basicView3.png|center]]
+
[[Image:RodinEditor_UserGuide_step4.png|600px]]
  
−
For more details, please go to the [[Rodin_Editor_User_Guide| Rodin Editor User Guide]].
+
Note that you can visualize the error message by going over the error marker with the mouse.
  
−
[[Category:Plugin]]
+
-- Enter the edition mode by clicking inside the label 'cst1'.
−
[[Category:User documentation]]
+
 
 +
[[Image:RodinEditor_UserGuide_step5.png]]
 +
 
 +
The overlay editor then appears (cst1 is in black, and the background is gray[see above]) and you can modify the label of the constant.<br>
 +
-- Modify the label to be 'k'and exit the overlay edition by pressing 'Enter'. ''Note that because 'Enter' is used to enter or exit the overlay mode under the caret, in order to insert carriage return in text, you have to press CTRL+ENTER.<br>''
 +
You can then save the file. <br>
 +
You then see something like the following.
 +
 
 +
[[Image:RodinEditor_UserGuide_step6.png]]
 +
 
 +
Then we want to add another constant. As we have 'k' already, we will use 'add sibling' command to add another constant after k.<br>
 +
-- Place the caret before k as on the following picture :
 +
 
 +
[[Image:RodinEditor_UserGuide_step7.png]]
 +
 
 +
-- Right-click. The following context menu appears :
 +
 
 +
[[Image:RodinEditor_UserGuide_step8.png|200px]]
 +
 
 +
-- Click on "Add Sibling" you see then that a new constant was created, named 'cst1'.
 +
 
 +
[[Image:RodinEditor_UserGuide_step9.png]]
 +
 
 +
You can then enter the overlay edition mode to change this value to 'c'
 +
 
 +
''' CONGRATULATIONS! You learned how to use the Rodin Editor.'''
 +
 
 +
=== Using keyboard shorcuts ===
 +
Here is the list of the currently key bindings which are set by default and specific to the Rodin Editor.
 +
 
 +
{{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)
 +
|}
 +
 
 +
=== 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.

Revision as of 13:18, 13 July 2011

Introduction

The Rodin Editor plug-in provides a structured editor to model in Event-B withing Rodin. This editor uses a textual representation, and edition is done through an overlay text editor and action depending on the caret position in the text.
For more details about the principles of this editor, see the Rodin Editor Plug-in page. IMPORTANT : we identified a source of concurrency issue in the current version (0.5.0) of the plug-in.
To avoid any trouble, please do not generate files while having some Rodin Editor open, and edit only one model per project at once.

Installation

Setup

Install the Rodin Editor plug-in:

  1. In the menu choose Help -> Install New Software...
  2. In the Work with dropdown list, choose the location URL: Rodin - http://rodin-b-sharp.sourceforge.net/updates
  3. Select the Rodin Editor feature then click the check box
  4. Click Next, after some time, the Install Details page appears
  5. Click Next and accept the license
  6. Click Finish
  7. A Security Warning window may appear: click OK
  8. Restart Rodin as suggested.

Now you are ready to use the new Rodin Editor plug-in.

Release Notes

See Rodin Editor Release Notes


Editing

This is a small exercice to get used to the principles of the new structured editor. It is based on the 'Celebrity' project of the tutorial. You can download the resulting project here.
We will here build the context Celebrity_C0.

Create a context, add elements to it

Let's create a Rodin project, and add a context component called Celebrity_C0 to it.
-- By opening this context with the Rodin Editor (right click > Open with > Rodin Editor) you shall obtain the following:
RodinEditor UserGuide step1.png

This editor allows to do things based on the position of the caret.
-- Place the caret at one location on the line of the context label, and before the label, as on the figure below:

RodinEditor UserGuide step2.png

-- Then right click, and add a 'Constant' child using the menus :

RodinEditor UserGuide step3.png

-- Save the file.
After saving the file, the error markers are recalculated, and you have an error that appears on the newly created constant 'cst1'.
You shall see this :

RodinEditor UserGuide step4.png

Note that you can visualize the error message by going over the error marker with the mouse.

-- Enter the edition mode by clicking inside the label 'cst1'.

RodinEditor UserGuide step5.png

The overlay editor then appears (cst1 is in black, and the background is gray[see above]) and you can modify the label of the constant.
-- Modify the label to be 'k'and exit the overlay edition by pressing 'Enter'. Note that because 'Enter' is used to enter or exit the overlay mode under the caret, in order to insert carriage return in text, you have to press CTRL+ENTER.
 You can then save the file.
You then see something like the following.

RodinEditor UserGuide step6.png

Then we want to add another constant. As we have 'k' already, we will use 'add sibling' command to add another constant after k.
-- Place the caret before k as on the following picture :

RodinEditor UserGuide step7.png

-- Right-click. The following context menu appears :

RodinEditor UserGuide step8.png

-- Click on "Add Sibling" you see then that a new constant was created, named 'cst1'.

RodinEditor UserGuide step9.png

You can then enter the overlay edition mode to change this value to 'c'

CONGRATULATIONS! You learned how to use the Rodin Editor.

Using keyboard shorcuts

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_Editor&oldid=7137’