Rodin Keyboard: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Nicolas |
imported>Nicolas |
||
| (One intermediate revision by the same user not shown) | |||
| Line 11: | Line 11: | ||
= Specification = | = Specification = | ||
{{TODO}} REWORK: rethink the specification, avoid regex, new design based on a [http://en.wikipedia.org/wiki/Trie Trie] data structure. | |||
Make a unique algorithm for all cases (Math + LaTeX + Text). | Make a unique algorithm for all cases (Math + LaTeX + Text). | ||
New ideas are: | New ideas are: | ||
| Line 18: | Line 18: | ||
* a text node is '''cuttable''' if it is not followed by an identifier part in the text to translate (see <code>org.eventb.internal.core.lexer.LexicalClass.IDENTIFIER</code>) | * a text node is '''cuttable''' if it is not followed by an identifier part in the text to translate (see <code>org.eventb.internal.core.lexer.LexicalClass.IDENTIFIER</code>) | ||
* a math node is always '''cuttable''' | * a math node is always '''cuttable''' | ||
* a node is '''translatable''' if it is both '''terminal''' AND '''cuttable''' | |||
* a node is '''translatable''' if it is both '''terminal''' AND ''' | * the translation consists in finding the longest translatable node in a text, starting from a given index, based on a trie that encodes the available combos; when the traversal exits the trie, we consider the latest translatable combo found: the translation is triggered if and only if the caret is not over it; then, the start index comes just after the corresponding translatable node and the translation goes on. | ||
* when | |||
<!-- | |||
== Definitions == | == Definitions == | ||
* '''Translator''': function that transforms a ('''source chain''', '''source caret position''') into a ('''target chain''', '''target caret position''') | * '''Translator''': function that transforms a ('''source chain''', '''source caret position''') into a ('''target chain''', '''target caret position''') | ||
| Line 169: | Line 169: | ||
* do not translate within an identifier, for instance 'NATURAL' must remain unchanged by translation, rather than 'ℕURAL' | * do not translate within an identifier, for instance 'NATURAL' must remain unchanged by translation, rather than 'ℕURAL' | ||
* do not translate a match that has the caret, so as to enable inputting identifiers that contain a combination input | * do not translate a match that has the caret, so as to enable inputting identifiers that contain a combination input | ||
--> | |||
[[Category:Design]] | [[Category:Design]] | ||
Latest revision as of 11:59, 23 June 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
TODO REWORK: rethink the specification, avoid regex, new design based on a Trie data structure. Make a unique algorithm for all cases (Math + LaTeX + Text). New ideas are:
- no translation if the caret is over a translatable combo (be it math/latex/text, even if it is the longest combo)
- a node is terminal if it holds a complete combo
- a text node is cuttable if it is not followed by an identifier part in the text to translate (see
org.eventb.internal.core.lexer.LexicalClass.IDENTIFIER) - a math node is always cuttable
- a node is translatable if it is both terminal AND cuttable
- the translation consists in finding the longest translatable node in a text, starting from a given index, based on a trie that encodes the available combos; when the traversal exits the trie, we consider the latest translatable combo found: the translation is triggered if and only if the caret is not over it; then, the start index comes just after the corresponding translatable node and the translation goes on.
