Difference between pages "Rodin Editor" and "Rodin Keyboard"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
imported>Nicolas
 
Line 1: Line 1:
−
{{TOCright}}
+
The Rodin Keyboard is an extensible keyboard for inputing mathematical formula (in Unicode).  The Rodin keyboard provides the following facilities:
−
Return to [[Rodin Plug-ins]]
+
* A ModifyListener (RodinModifyListener) that can be attached to a SWT widget. When the content of the widget is modified, the keyboard reacts and translate the content accordingly. Currently, RODIN Keyboard supports Text and StyledText widget.
 +
* An utility class Text2MathTranslator with a static method translate(String) for manually translating any string (or sub-part of a string) into mathematical formula.
 +
* An Eclipse View called Rodin Keyboard View which provides an text input area which will translate the input text into mathematical formula. This View can be found under category RODIN.
  
−
[[Image:RodinEditor_basicView1.png|400px|left|a basic view of the Rodin Editor on a context]]
+
The Rodin Keyboard however does not contain any pre-defined translation rules for any mathematical symbols. Instead, this task is left for the developers who want to declare different "keyboards" corresponding to the mathematical language that they want to use. Moreover, different combinations can be used to enter the same mathematical symbols.
  
−
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.
+
Currently, there are two keyboards available:
 +
* Standard keyboard for Event-B.
 +
* LaTeX-style keyboard for Event-B.
  
−
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.
+
= Specification =
−
<br style="clear: both" />
 
  
−
=== Installation Details ===
+
== Definitions ==
−
{{TODO}} Document this part when the plug-in is released.
+
* '''Translator''': mechanism that transforms a '''source chain''' into a '''target chain''' according to a set of '''transformation rules'''
 +
* '''Token''': '''isolated''' character sequence in a chain
 +
* '''Transformation Rule''': specification of the modification of a token sequence into another token sequence
 +
* '''Combination''': specification of a transformation from a single input token into another single output token
 +
* There are 3 kinds of lexical entities in a source chain:
 +
** '''spacings''' (space, tabulation, end of line, ...)
 +
** '''text symbols''' (identifier-like)
 +
** '''math symbols''' (all other symbols)
  
−
=== Principles ===
+
== Requirements ==
−
'''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:
+
# The translator must be able to deal both with static translation of a whole chain and on the fly translation of a user input chain (characters being typed in continuously)
−
* 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,
+
# The translator must help maintain a coherent caret position
−
* you can edit the Event-B element's attributes by entering the "edition" mode provided by the overlay editor. This is detailed here-after.
+
# The translator must keep spacing unchanged
 +
# The translator must support contributed combinations
 +
# The translator must avoid non-termination due to combination contributions
 +
#: This will be enforced by a stronger requirement: the translation must be an idempotent operation for a given caret position, for whatever contributed combinations
 +
# The translator must check that combination input tokens are either identifier-like or other symbols
 +
# The translator must not process a token that has the caret over it
 +
# Once a symbol has been translated, it can never be translated back into its original text form
  
−
'''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:
+
[[Category:Design]]
−
* 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.<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.
 
−
 
 
−
=== Available keyboard shortcurts ===
 
−
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.
 
−
 
 
−
[[Category:Plugin]]
 
−
[[Category:User documentation]]
 

Revision as of 15:41, 28 January 2014

The Rodin Keyboard is an extensible keyboard for inputing mathematical formula (in Unicode). The Rodin keyboard provides the following facilities:

  • A ModifyListener (RodinModifyListener) that can be attached to a SWT widget. When the content of the widget is modified, the keyboard reacts and translate the content accordingly. Currently, RODIN Keyboard supports Text and StyledText widget.
  • An utility class Text2MathTranslator with a static method translate(String) for manually translating any string (or sub-part of a string) into mathematical formula.
  • An Eclipse View called Rodin Keyboard View which provides an text input area which will translate the input text into mathematical formula. This View can be found under category RODIN.

The Rodin Keyboard however does not contain any pre-defined translation rules for any mathematical symbols. Instead, this task is left for the developers who want to declare different "keyboards" corresponding to the mathematical language that they want to use. Moreover, different combinations can be used to enter the same mathematical symbols.

Currently, there are two keyboards available:

  • Standard keyboard for Event-B.
  • LaTeX-style keyboard for Event-B.

Specification

Definitions

  • Translator: mechanism that transforms a source chain into a target chain according to a set of transformation rules
  • Token: isolated character sequence in a chain
  • Transformation Rule: specification of the modification of a token sequence into another token sequence
  • Combination: specification of a transformation from a single input token into another single output token
  • There are 3 kinds of lexical entities in a source chain:
    • spacings (space, tabulation, end of line, ...)
    • text symbols (identifier-like)
    • math symbols (all other symbols)

Requirements

  1. The translator must be able to deal both with static translation of a whole chain and on the fly translation of a user input chain (characters being typed in continuously)
  2. The translator must help maintain a coherent caret position
  3. The translator must keep spacing unchanged
  4. The translator must support contributed combinations
  5. The translator must avoid non-termination due to combination contributions
    This will be enforced by a stronger requirement: the translation must be an idempotent operation for a given caret position, for whatever contributed combinations
  6. The translator must check that combination input tokens are either identifier-like or other symbols
  7. The translator must not process a token that has the caret over it
  8. Once a symbol has been translated, it can never be translated back into its original text form
Retrieved from ‘https://wiki.event-b.org/index.php?title=Rodin_Editor&oldid=7220’