Difference between revisions of "Event-B XText Front-end User Guide"

From Event-B
Jump to: navigation, search
m (Editing)
Line 21: Line 21:
== Editing ==
== 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 [http://sourceforge.net/projects/rodin-b-sharp/files/Doc_%20Tutorial/1.1/Celebrity.zip/download <tt>here</tt>].<br>
== Converting Rodin files to Event-B XText ==
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.<br>
-- By opening this context with the Rodin Editor (right click > Open with > Rodin Editor) you shall obtain the following:<br>
This editor allows to do things based on the position of the caret.<br>
-- The caret is place at the front of the context name, and this is fine because we want to add a constant
to the context.
-- To add a constant, right click and select '[Child]-> Add Constant' as in the picture below:
-- Save the file. <br>
After saving the file, the error markers are recalculated, and you have an error that appears on the newly created constant 'cst1'.<br>
You shall see something like this :
Note that you can visualize the error message by going over the error marker with the mouse.
-- Now we enter the edition mode by clicking inside the label 'cst1', as we want to name the constant 'cst1' to 'k'.
The overlay editor then appears (the background is grey and a box is drawn[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' or click next to k. ''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 (Apple+Enter) on mac platforms.<br>''
You can then save the file. <br>
You then see something like the following.
Then we want to give this constant an integer type. As the caret is near 'k', and k is a constant, we will use '[Sibling]-> Add sibling' command to add an axiom.<br>
-- Right-click and select "[Sibling]-> Add Axiom" you see then that a new axiom was created, named 'axm1'.
You've just created an axiom that you can edit to give the constant k a type.
You can then enter the overlay edition mode to change this value to 'k : INT'.<br>
After saving the file, you obtain the following context :
and the markers disappear because there is no error left in your context.
Finally, suppose that the axiom axm1 should be considered as a theorem, click on not theorem after the axiom formula, to change the attribute of the predicate to a theorem.
''' CONGRATULATIONS! You learned how to use the Rodin Editor.'''
You learned that :
# To create an element:
## or you place the caret before the label of its parent, and create a child using '[Child]->Add xxx' where xxx is the type of element you want to add, from the contextual menu,
## or you place the caret next to a sibling element and you create a sibling using '[Sibling]->Add xxx' where xxx is the type of element you want to add, from the contextual menu.
# To edit the attributes of an element:
## you enter the overlay edition with left click or with "ENTER" and modify the textual contents,
## you press 'ENTER' to quit overlay edition (or click outside the overlay editor).
=== Select, Move and delete elements ===
-- To select elements, you have 3 choices:
* you can double-click on them,
* or press CTRL and click on one element,
* or click on the visual circle handle at their left.
The selected elements appear with a blue background,
or a gray background if they are of different types. See the picture below.
-- To unselect element, by default, press ESC.
-- To move elements, try both:
* Move Up and Move Down commands in the context menu, once elements are selected,
* Drag and drop on the selection.
-- To delete elements, try both:
* Use the 'Delete' command on a selection from the context menu,
* Press the DEL or SUPPR key after selecting the elements you want to delete.
=== Using keyboard shorcuts ===
Here is the list of the currently key bindings which are set by default and specific to the Rodin Editor.
! 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
| ALT+T || Add a sibling of the element pointed by the caret position. The sibling is placed just after this latter one.
| ALT+G || 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.
| 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 these shortcuts ===
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 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 16:49, 4 November 2016


The Event-B XText front-end provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines.
For more details about the principles of this editor, see the Event-B XText Front-end page.



Release Notes

See Event-B XText Front-end Release Notes


  • Currently, Event-B XText front-end ONLY supports "standard" Event-B machines and contexts.
  • Since the XContexts and XMachines are compiled to the Rodin files, the corresponding Rodin contexts and machines will be OVER-WRITTEN. Any changes in the Rodin files will not be lost.
  • DO NOT USE the Event-B XText Front-end if you use modelling plug-ins such as iUML-B state-machines and class-diagrams, as the additional modelling elements will be over-written.


Converting Rodin files to Event-B XText