Rodin Keyboard User Guide - Revision history

imported>Laurent: /* Extending the Keyboard */ Updated example and text

2010-07-21T12:58:00Z

Extending the Keyboard: Updated example and text

← Older revision		Revision as of 12:58, 21 July 2010
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 ==

imported>Laurent: Renamed "RODIN Keyboard" to "Rodin Keyboard".

2010-07-21T12:31:41Z

Renamed "RODIN Keyboard" to "Rodin Keyboard".

← Older revision		Revision as of 12:31, 21 July 2010
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 194:		Line 194:

	== 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 231:		Line 231:

	=== 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.

imported>Pascal: /* Useless nowiki tag have been removed. */

2010-02-19T17:02:30Z

Useless nowiki tag have been removed.

imported>Pascal: /* Special Combos */

2010-02-19T15:11:05Z

Special Combos

← Older revision		Revision as of 15:11, 19 February 2010
Line 19:		Line 19:
	Below are the special combos (set of ASCII characters) and their translations into the Event-B mathematical language.		Below are the special combos (set of ASCII characters) and their translations into the Event-B mathematical language.

	{\| border="1"		{\| border="1" cellspacing="0"
	! ASCII !! LaTeX !! Math !! Meaning !! Unicode		! ASCII !! LaTeX !! Math !! Meaning !! Unicode
	\|-		\|-

imported>Pascal: /* Revert */

2010-02-19T15:04:42Z

Revert

← Older revision		Revision as of 15:04, 19 February 2010
Line 1:		Line 1:
	{~~\| cellspacing="0" cellpadding="0" style="clear: right; margin-bottom: .5em; float: right; padding: .5em 0 .8em 1.4em; background: none; width: auto;"~~ {~~{#if:\|class="toclimit-{{{limit}}}"}~~}		{{TOCright}}
	~~\| __TOC__~~
	\|}

	== Introduction ==		== Introduction ==
Line 21:		Line 19:
	Below are the special combos (set of ASCII characters) and their translations into the Event-B mathematical language.		Below are the special combos (set of ASCII characters) and their translations into the Event-B mathematical language.

	{\|~~class="SimpleTable" text-align="center"~~ border="1" ~~cellspacing="4" cellpadding="8" rules="all" frame="box" style="margin:1em 1em 1em 0; border-style:solid; border-color:#AAAAAA; display:inline-table; "~~		{\| border="1"

	! ASCII !! LaTeX !! Math !! Meaning !! Unicode		! ASCII !! LaTeX !! Math !! Meaning !! Unicode
	\|-		\|-
Line 250:		Line 247:
	== Samples ==		== Samples ==
	=== Expression ===		=== Expression ===
	~~<span style="background-color:yellow;">'''TODO'''</span>~~{{~~#if: \|<nowiki>: </nowiki>''{{{1}}}''~~}}		{{TODO}}

	=== Jumping ===		=== Jumping ===
	~~<span style="background-color:yellow;">'''TODO'''</span>~~{{~~#if: \|<nowiki>: </nowiki>''{{{1}}}''~~}}		{{TODO}}

	[[Category:User documentation]]		[[Category:User documentation]]
	[[Category:Work in progress]]		[[Category:Work in progress]]

imported>Pascal at 15:02, 19 February 2010

2010-02-19T15:02:34Z

← Older revision		Revision as of 15:02, 19 February 2010
Line 1:		Line 1:

	{\| cellspacing="0" cellpadding="0" style="clear: right; margin-bottom: .5em; float: right; padding: .5em 0 .8em 1.4em; background: none; width: auto;" {{#if:\|class="toclimit-{{{limit}}}"}}		{\| cellspacing="0" cellpadding="0" style="clear: right; margin-bottom: .5em; float: right; padding: .5em 0 .8em 1.4em; background: none; width: auto;" {{#if:\|class="toclimit-{{{limit}}}"}}
	\| __TOC__		\| __TOC__

imported>Pascal: /* Template substitution, to transform this page to Eclipse Help using Wiki2Help */

2010-02-19T14:58:39Z

Template substitution, to transform this page to Eclipse Help using Wiki2Help

← Older revision		Revision as of 14:58, 19 February 2010
Line 1:		Line 1:
	{{~~TOCright~~}}
			{\| cellspacing="0" cellpadding="0" style="clear: right; margin-bottom: .5em; float: right; padding: .5em 0 .8em 1.4em; background: none; width: auto;" {{#if:\|class="toclimit-{{{limit}}}"}}
			\| __TOC__
			\|}

	== Introduction ==		== Introduction ==
Line 248:		Line 251:
	== Samples ==		== Samples ==
	=== Expression ===		=== Expression ===
	{{~~TODO~~}}		<span style="background-color:yellow;">'''TODO'''</span>{{#if: \|<nowiki>: </nowiki>''{{{1}}}''}}

	=== Jumping ===		=== Jumping ===
	{{~~TODO~~}}		<span style="background-color:yellow;">'''TODO'''</span>{{#if: \|<nowiki>: </nowiki>''{{{1}}}''}}

	[[Category:User documentation]]		[[Category:User documentation]]
	[[Category:Work in progress]]		[[Category:Work in progress]]

imported>Pascal: /* Special Combos */

2010-02-19T14:54:33Z

Special Combos

← Older revision		Revision as of 14:54, 19 February 2010
Line 18:		Line 18:
	=== Special Combos ===		=== Special Combos ===
	Below are the special combos (set of ASCII characters) and their translations into the Event-B mathematical language.		Below are the special combos (set of ASCII characters) and their translations into the Event-B mathematical language.
	{~~{SimpleHeader}}~~
			{\|class="SimpleTable" text-align="center" border="1" cellspacing="4" cellpadding="8" rules="all" frame="box" style="margin:1em 1em 1em 0; border-style:solid; border-color:#AAAAAA; display:inline-table; "

	! ASCII !! LaTeX !! Math !! Meaning !! Unicode		! ASCII !! LaTeX !! Math !! Meaning !! Unicode
	\|-		\|-

imported>Pascal: /* RODIN Keyboard View */

2010-02-19T13:39:28Z

RODIN Keyboard View

← Older revision		Revision as of 13:39, 19 February 2010
Line 199:		Line 199:

	<center>		<center>
	[[Image:RODIN_keyboard_view.~~jpg~~]]		[[Image:RODIN_keyboard_view.png]]
	</center>		</center>

imported>Pascal: /* Useless font id have been removed */

2010-02-18T13:56:56Z

Useless font id have been removed

← Older revision		Revision as of 13:56, 18 February 2010
Line 16:		Line 16:
	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).

	=== ~~<font id="combos">~~ Special Combos ~~</font>~~ ===		=== Special Combos ===
	Below are the special combos (set of ASCII characters) and their translations into the Event-B mathematical language.		Below are the special combos (set of ASCII characters) and their translations into the Event-B mathematical language.
	{{SimpleHeader}}		{{SimpleHeader}}
Line 204:		Line 204:
	== 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 [[#~~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 ===
	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.		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 [[#~~pref~~ \| here]].		More information about the Preferences page can be found [[#Preferences \| here]].

	=== Extending the Keyboard ===		=== Extending the Keyboard ===
Line 229:		Line 229:
	See the [http://wiki.event-b.org/index.php/Keyboard_Release_History Keyboard Release History].		See the [http://wiki.event-b.org/index.php/Keyboard_Release_History Keyboard Release History].

	=== ~~<font id="pref">~~ Preferences ~~</font>~~===		=== 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.

← Older revision		Revision as of 17:02, 19 February 2010
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" \|		\|colspan="5" \|
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
	\|}		\|}