Difference between revisions of "Rodin Keyboard User Guide"

From Event-B
Jump to navigationJump to search
imported>Pascal
imported>Laurent
(→‎Extending the Keyboard: Updated example and text)
 
(2 intermediate revisions by 2 users not shown)
Line 7: Line 7:
 
== Getting Started ==
 
== Getting Started ==
 
=== Overview ===
 
=== Overview ===
The Rodin Keyboard plug-in creates a view (namely "RODIN Keyboard") under Event-B category.
+
The Rodin Keyboard plug-in creates a view (namely "Rodin Keyboard") under Event-B category.
  
You can open "RODIN Keyboard" view now:  
+
You can open "Rodin Keyboard" view now:  
  
 
# Go to Window/Show View/Other.  
 
# Go to Window/Show View/Other.  
# Choose the "RODIN Keyboard" view from the Event-B category.  
+
# Choose the "Rodin Keyboard" view from the Event-B category.  
  
 
The view contains a text area which takes an ASCII input and translate it into the mathematical language (defined by extensions).
 
The view contains a text area which takes an ASCII input and translate it into the mathematical language (defined by extensions).
Line 144: Line 144:
 
|align="center" | <code>><</code> || align="center" | \dprod || align="center" | <math>\dprod</math> || Direct product || U+2297
 
|align="center" | <code>><</code> || align="center" | \dprod || align="center" | <math>\dprod</math> || Direct product || U+2297
 
|-
 
|-
|align="center" | <code><nowiki>||</nowiki></code> || align="center" | \pprod || align="center" | <math>\pprod</math> || Parallel product || U+2225
+
|align="center" | <code>|</code><code>|</code> || align="center" | \pprod || align="center" | <math>\pprod</math> || Parallel product || U+2225
 
|-
 
|-
 
|align="center" | <code>~</code> || align="center" | \conv || align="center" | ~ || Tilde operator || U+223C
 
|align="center" | <code>~</code> || align="center" | \conv || align="center" | ~ || Tilde operator || U+223C
 
|-
 
|-
|align="center" | <code><nowiki><|</nowiki></code> || align="center" | \domres || align="center" | <math>\domres</math> || Domain restriction || U+25C1
+
|align="center" | <code><|</code> || align="center" | \domres || align="center" | <math>\domres</math> || Domain restriction || U+25C1
 
|-
 
|-
|align="center" | <code><nowiki><<|</nowiki></code> || align="center" | \domsub || align="center" | <math>\domsub</math> || Domain subtraction || U+2A64
+
|align="center" | <code><<|</code> || align="center" | \domsub || align="center" | <math>\domsub</math> || Domain subtraction || U+2A64
 
|-
 
|-
 
|align="center" | <code>|></code> || align="center" | \ranres || align="center" | <math>\ranres</math> || Range restriction || U+25B7
 
|align="center" | <code>|></code> || align="center" | \ranres || align="center" | <math>\ranres</math> || Range restriction || U+25B7
Line 164: Line 164:
 
|align="center" | <code>UNION</code> || align="center" | \Union || align="center" | <math>\Union</math> || N-ary union || U+22C3
 
|align="center" | <code>UNION</code> || align="center" | \Union || align="center" | <math>\Union</math> || N-ary union || U+22C3
 
|-
 
|-
|align="center" | <code><nowiki>|</nowiki></code> || align="center" | \mid || align="center" | <math>\mid</math> || Such that || U+2223
+
|align="center" | <code>|</code> || align="center" | \mid || align="center" | <math>\mid</math> || Such that || U+2223
 
|-
 
|-
 
|colspan="5" | &nbsp;
 
|colspan="5" | &nbsp;
Line 190: Line 190:
 
|align="center" | <code>::</code> || align="center" | \bcmin || align="center" | <math>\bcmin</math> || Becomes an element of || U+003A U+2208  
 
|align="center" | <code>::</code> || align="center" | \bcmin || align="center" | <math>\bcmin</math> || Becomes an element of || U+003A U+2208  
 
|-
 
|-
|align="center" | <code><nowiki>:|</nowiki></code> || align="center" | \bcmsuch || align="center" | <math>\bcmsuch</math> || Becomes such that || U+003A U+2223
+
|align="center" | <code>:|</code> || align="center" | \bcmsuch || align="center" | <math>\bcmsuch</math> || Becomes such that || U+003A U+2223
 
|}
 
|}
  
 
== Concepts ==
 
== Concepts ==
=== RODIN Keyboard View ===
+
=== Rodin Keyboard View ===
 
The view contains a text area where ASCII input can be typed in. The text will be translated into the mathematical language (which is extensible) when there is a modification of the text. The translation is done for the whole text spanned over multiple lines.  
 
The view contains a text area where ASCII input can be typed in. The text will be translated into the mathematical language (which is extensible) when there is a modification of the text. The translation is done for the whole text spanned over multiple lines.  
  
Line 205: Line 205:
 
== Tasks ==
 
== Tasks ==
 
=== Entering a Mathematical Formula ===
 
=== Entering a Mathematical Formula ===
A formula in the mathematical language of Event-B can be typed in the text area of the RODIN Keyboard view. The view will translate the formula from ASCII into the mathematical language as specified [[#Special_Combos | here]]. The formula can be copied as normal (Unicode) text.
+
A formula in the mathematical language of Event-B can be typed in the text area of the Rodin Keyboard view. The view will translate the formula from ASCII into the mathematical language as specified [[#Special_Combos | here]]. The formula can be copied as normal (Unicode) text.
  
 
=== Changing the Font ===
 
=== Changing the Font ===
Line 213: Line 213:
  
 
=== Extending the Keyboard ===
 
=== Extending the Keyboard ===
There is an extension point to extend the keyboard namely <tt>org.rodinp.keyboard.symbols</tt>. An example of this extension point is shown below.
+
There is an extension point to extend the keyboard namely <tt>org.rodinp.keyboard.symbols</tt>. An example of using this extension point is shown below.
  
  <extension point="org.eventb.eventBKeyboard.translators">
+
  <extension
<translator
+
    point="org.rodinp.keyboard.symbols">
class="org.eventb.eventBKeyboard.views.EventBKeyboardTextTranslator">
+
    <symbol
</translator>
+
combo="not"
<translator
+
id="neg"
class="org.eventb.eventBKeyboard.views.EventBKeyboardMathTranslator">
+
name="%negName"
</translator>
+
translation="¬" />
 +
    <symbolProvider
 +
class="my.package.name.MyClassProvidingSymbols" />
 
  </extension>
 
  </extension>
  
The class attribute must be a fully qualified name of the class that implements <tt>org.eventb.eventBKeyboard.views.IEventBKeyboardTranslator</tt>. It involves to implement the abstract <tt>translate(Text widget)</tt> method. An example can be taken from <tt>org.eventb.eventBKeyboard.views.EventBKeyboardTextTranslator</tt> or <tt>org.eventb.eventBKeyboard.views.EventBKeyboardMathTranslator</tt>.  
+
The first extension contributes a symbol with all the details for translating an ASCII combination into a symbol. The second extension contributes a class. This class will be instantiated by the Rodin Keyboard plug-in to fetch additional symbol definitions. This allows for contributing new symbols dynamically.
  
 
== Reference ==
 
== Reference ==
Line 231: Line 233:
  
 
=== Preferences ===
 
=== Preferences ===
The Preferences page is used to change the font of the text area in the RODIN Keyboard view. You can access it from the "General/Appearance/Colors and Fonts" page.
+
The Preferences page is used to change the font of the text area in the Rodin Keyboard view. You can access it from the "General/Appearance/Colors and Fonts" page.
  
 
A sample of this preferences page is shown below.
 
A sample of this preferences page is shown below.

Latest revision as of 12:58, 21 July 2010

Introduction

This short help page provides necessary information on the Rodin Keyboard plug-in and also on how to extend the plug-in.

Getting Started

Overview

The Rodin Keyboard plug-in creates a view (namely "Rodin Keyboard") under Event-B category.

You can open "Rodin Keyboard" view now:

  1. Go to Window/Show View/Other.
  2. Choose the "Rodin Keyboard" view from the Event-B category.

The view contains a text area which takes an ASCII input and translate it into the mathematical language (defined by extensions).

Special Combos

Below are the special combos (set of ASCII characters) and their translations into the Event-B mathematical language.

ASCII LaTeX Math Meaning Unicode
NAT \nat \nat The set of natural numbers U+2115
NAT1 \natn \natn The set of positive natural numbers U+2115 U+0031
INT \intg \intg The set of integer numbers U+2124
POW \pow \pow The set of all subsets (power set) U+2119
POW1 \pown \pown The set of all non-empty subsets U+2119 U+0031
 
( ( ( Left parenthesis U+0028
) ) ) Right parenthesis U+0029
<=> \leqv \leqv Logical equivalence U+21D4
=> \limp \limp Logical implication U+21D2
& \land \land Logical conjunction U+2227
or \lor \lor Logical disjunction U+2228
not \lnot \lnot Not sign U+00AC
true \btrue \btrue True predicate U+22A4
false \bfalse \bfalse False predicate U+22A5
! \forall \forall For all U+2200
# \exists \exists There exists U+2203
, , , Comma U+002C
. \qdot \qdot Middle dot U+00B7
 
= = = Equal to U+003D
/= \neq \neq Not equal to U+2260
< < < Less than U+003C
<= \leq \leq Less than or equal to U+2264
> > > Greater than U+003E
>= \geq \geq Greater than or equal to U+2265
: \in \in Element of U+2208
/: \notin \notin Not an element of U+2209
<<: \subset \subset (Proper) Subset of U+2282
/<<: \notsubset \not\subset Not a (proper) subset of U+2284
<: \subseteq \subseteq Subset of or equal to U+2286
/<: \notsubseteq \not\subseteq Neither a subset of nor equal to U+2288
 
<-> \rel \rel Relation U+2194
<<-> \trel \trel Total relation U+E100
<->> \srel \srel Surjective relation U+E101
<<->> \strel \strel Total surjective relation U+E102
+-> \pfun \pfun Partial function U+21F8
--> \tfun \tfun Total function U+2192
>+> \pinj \pinj Partial injection U+2914
>-> \tinj \tinj Total injection U+21A3
+>> \psur \psur Partial surjection U+2900
->> \tsur \tsur Total surjection U+21A0
>->> \tbij \tbij Bijection U+2916
 
{ { { Left curly bracket U+007B
} } } Right curly bracket U+007D
|-> \mapsto \mapsto Maplet U+21A6
,,
{} \emptyset \emptyset Empty set U+2205
/\ \binter \binter Intersection U+2229
\/ \bunion \bunion Union U+222A
\ \setminus \setminus Set minus U+2216
** \cprod \cprod Cartesian product U+00D7
 
[ [ [ Left square bracket U+005B
] ] ] Right square bracket U+005D
<+ \ovl \ovl Relation overriding U+E103
circ \bcomp \bcomp Backward composition U+2218
; \fcomp \fcomp Forward composition U+003B
>< \dprod \dprod Direct product U+2297
|| \pprod \pprod Parallel product U+2225
~ \conv ~ Tilde operator U+223C
<| \domres \domres Domain restriction U+25C1
<<| \domsub \domsub Domain subtraction U+2A64
|> \ranres \ranres Range restriction U+25B7
|>> \ransub \ransub Range subtraction U+2A65
 
% \lambda \lambda Lambda U+03BB
INTER \Inter \Inter N-ary intersection U+22C2
UNION \Union \Union N-ary union U+22C3
| \mid \mid Such that U+2223
 
.. \upto \upto Upto sign U+2025
+ + + Addition sign U+002B
- - - Subtraction sign U+2212
* * * Multiplication sign U+2217
/ \div \div Division sign U+00F7
^ \expn \expn Exponentiation sign U+005E
 
oftype \oftype Oftype.png Typing operator U+2982
 
:= \bcmeq \bcmeq Becomes equal to U+2254
:: \bcmin \bcmin Becomes an element of U+003A U+2208
:| \bcmsuch \bcmsuch Becomes such that U+003A U+2223

Concepts

Rodin Keyboard View

The view contains a text area where ASCII input can be typed in. The text will be translated into the mathematical language (which is extensible) when there is a modification of the text. The translation is done for the whole text spanned over multiple lines.

Below is an example of the view which is attached to the bottom area of the workbench.

RODIN keyboard view.png

Tasks

Entering a Mathematical Formula

A formula in the mathematical language of Event-B can be typed in the text area of the Rodin Keyboard view. The view will translate the formula from ASCII into the mathematical language as specified here. The formula can be copied as normal (Unicode) text.

Changing the Font

In order to display the Unicode characters for the mathematical language, there is a special font associated with the text area. This font can be changed in the Preferences page associated with the Colors and Fonts. It can be opened from the category "General/Appearance/Colors And Fonts". Any font can be chosen, but mathematical language formulas can be displayed correctly only if the chosen font contains the Unicode characters for the mathematical language. From the Preferences page, you can choose the font, the style and the size for the text area.

More information about the Preferences page can be found here.

Extending the Keyboard

There is an extension point to extend the keyboard namely org.rodinp.keyboard.symbols. An example of using this extension point is shown below.

<extension
    point="org.rodinp.keyboard.symbols">
    <symbol
	combo="not"
	id="neg"
	name="%negName"
	translation="¬" />
    <symbolProvider
	class="my.package.name.MyClassProvidingSymbols" />
</extension>

The first extension contributes a symbol with all the details for translating an ASCII combination into a symbol. The second extension contributes a class. This class will be instantiated by the Rodin Keyboard plug-in to fetch additional symbol definitions. This allows for contributing new symbols dynamically.

Reference

Release Notes

See the Keyboard Release History.

Preferences

The Preferences page is used to change the font of the text area in the Rodin Keyboard view. You can access it from the "General/Appearance/Colors and Fonts" page.

A sample of this preferences page is shown below.

Keyboard preferences.jpg

The button "Change Font" is used to choose a new font. A pop-up dialog will be open and you can choose from the set of system fonts. The button "Reset" is used to set the font to the default Brave Sans Mono font.

There are four other buttons at the bottom of the page:

  • Restore Default: Restore the default fonts. It does not affect the Keyboard view.
  • Apply: Apply the current chosen font for the Keyboard view.
  • OK: Store the preference values to the preference store and close the page. It also applies the current chosen font for the Keyboard view.
  • Cancel: Close the page immediately without saving the preference values. Obviously, this does not affect the Keyboard view.

Samples

Expression

TODO

Jumping

TODO