Rodin Keyboard - Revision history

imported>Nicolas: /* Specification */

2014-06-23T11:59:52Z

Specification

← Older revision		Revision as of 11:59, 23 June 2014
Line 21:		Line 21:
	* 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.		* 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.

			<!--
	== 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]]

imported>Nicolas: /* Specification */

2014-06-23T11:58:32Z

Specification

← Older revision		Revision as of 11:58, 23 June 2014
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.		{{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 '''cut''' if it is cuttable and the caret is not over the combo it holds		* a node is '''translatable''' if it is both '''terminal''' AND '''cuttable'''
	* a node is '''translatable''' if it is both '''terminal''' AND '''~~cut~~'''		* 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 ~~failing to translate a cut node~~, we ~~fall back to translating~~ the ~~previous~~ translatable node

	== Definitions ==		== Definitions ==

imported>Nicolas: /* Specification */

2014-06-23T11:36:45Z

Specification

← Older revision		Revision as of 11:36, 23 June 2014
Line 17:		Line 17:
	* a node is '''terminal''' if it holds a complete 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 <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 '''cuttable''' ~~if it is not followed by one of its child keys (or if it has no child keys in the trie)~~		* a math node is always '''cuttable'''
	* a node is '''cut''' if it is cuttable and the caret is not over the combo it holds		* a node is '''cut''' if it is cuttable and the caret is not over the combo it holds
	* a node is '''translatable''' if it is both '''terminal''' AND '''cut'''		* a node is '''translatable''' if it is both '''terminal''' AND '''cut'''

imported>Nicolas: /* Specification */

2014-06-23T10:48:44Z

Specification

← Older revision		Revision as of 10:48, 23 June 2014
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.		*{{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:
	* no translation if the caret is over a translatable combo (be it math/latex/text, even if it is the longest combo)		* no translation if the caret is over a translatable combo (be it math/latex/text, even if it is the longest combo)
	* a text node in the ~~Trie~~ (see <code>org.eventb.internal.core.lexer.LexicalClass.IDENTIFIER</code>~~, concerns both LaTeX and Text combos~~) ~~may be~~ a ~~terminal~~ node ~~(that triggers translation) only~~ if followed by ~~a non identifier part~~ in the ~~text to translate (i.e, we consider as a child key of a text node all identifier part characters, implemented as a node that loops over itself and consumes an identifier~~)		* a node is '''terminal''' if it holds a complete combo
	* a ~~math node may always be a terminal~~ node		* 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 node is translatable if:		* a math node is '''cuttable''' if it is not followed by one of its child keys (or if it has no child keys in the trie)
	~~:~~ it is a terminal ~~node~~ AND		* a node is '''cut''' if it is cuttable and the caret is not over the combo it holds
	~~: the lookahead character in the text~~ to translate ~~is not a child key~~		* a node is '''translatable''' if it is both '''terminal''' AND '''cut'''
	* translation is triggered on a node ~~if:~~		* when failing to translate a cut node, we fall back to translating the previous translatable node
	: it is a translatable node ~~AND~~
	: the caret is not over the translatable combo

	== Definitions ==		== Definitions ==

imported>Nicolas at 10:00, 23 June 2014

2014-06-23T10:00:02Z

← Older revision		Revision as of 10:00, 23 June 2014
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).
			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 text node in the Trie (see <code>org.eventb.internal.core.lexer.LexicalClass.IDENTIFIER</code>, concerns both LaTeX and Text combos) may be a terminal node (that triggers translation) only if followed by a non identifier part in the text to translate (i.e, we consider as a child key of a text node all identifier part characters, implemented as a node that loops over itself and consumes an identifier)
			* a math node may always be a terminal node
			* a node is translatable if:
			: it is a terminal node AND
			: the lookahead character in the text to translate is not a child key
			* translation is triggered on a node if:
			: it is a translatable node AND
			: the caret is not over the translatable combo

	== Definitions ==		== Definitions ==

imported>Nicolas: /* Requirements */

2014-06-20T16:11:21Z

Requirements

← Older revision		Revision as of 16:11, 20 June 2014
Line 41:		Line 41:
	# The translator must check that combination output tokens are not a substring of any input token; this enforces one-pass termination of the translation		# The translator must check that combination output tokens are not a substring of any input token; this enforces one-pass termination of the translation
	# The translator must not process a text token that has the caret over it		# The translator must not process a text token that has the caret over it
	# The ~~translator must process~~ a ~~math token~~ (w or ~~w/o the~~ caret over ~~it) that is the longest possible input combination~~		# The caret is over a substring if it is next to any character of the substring (left, right or both): there are 3 caret positions over "ab"
	# Once a symbol has been translated, it can never be translated ~~back~~ into ~~its original text form (even virtually during a translation)~~		# Once a symbol has been translated, the translation itself it can never be translated into anything else
	# The translator must not process a language token, like ':∈' or '$POW' (but we may concede an exception for predicate variables for simplicity)		# The translator must not process a language token, like ':∈' or '$POW' (but we may concede an exception for predicate variables for simplicity)

imported>Nicolas: /* Functional Needs */

2014-06-20T16:01:27Z

Functional Needs

← Older revision		Revision as of 16:01, 20 June 2014
Line 29:		Line 29:
	# Support statically contributed combinations (add)		# Support statically contributed combinations (add)
	# Support dynamically contributed combinations (check validity, add and remove, will be useful for theories)		# Support dynamically contributed combinations (check validity, add and remove, will be useful for theories)
	#:~~+ maybe handle a~~ scope ~~? could help~~ when ~~working with 2 projects that define the same~~ combination input for different ~~outputs~~		#:But no notion of scope; when proposed an already existing combination input for a different output, the newer one must be refused (invalid), the user shall close the project with the offending combination in order to replace it.
	# Avoid non-termination cases (combinations that produce input of combinations)		# Avoid non-termination cases (combinations that produce input of combinations)

imported>Nicolas: /* Math Translation */

2014-05-21T17:31:25Z

Math Translation

← Older revision		Revision as of 17:31, 21 May 2014
Line 116:		Line 116:

	if i equals length of matched:		if i equals length of matched:
	return translation		return (translation, pending_translation, caretShift)

	// i is now at start of a combination input		// i is now at start of a combination input

imported>Nicolas: /* Algorithm */

2014-05-21T17:30:08Z

Algorithm

@@ Line 55: / Line 55: @@
 Only search for first match, translate, then search for other matches in translated text repeatedly.
-=== Math Translation (regular or LaTeX style) ===
+=== LaTeX Style Translation ===
 Translate first longest substrings of matched part that equals a math input combination.
-Given text 'matched' to translate and caret position 'caret' (translated to fit inside 'matched', if needed):
+Given text 'matched' to translate and caret position 'caret' (translated to 'matched', (== original caret position in whole text minus index of 'matched')):
 <pre>
@@ Line 112: / Line 154: @@
 </pre>
 === Text Translations ===

imported>Nicolas: /* Requirements */

2014-05-21T16:47:43Z

Requirements

← Older revision		Revision as of 16:47, 21 May 2014
Line 38:		Line 38:
	#: A combination input is a valid math token if it matches either:		#: A combination input is a valid math token if it matches either:
	#:* <pre>[^a-zA-Z0-9_\s]+</pre>		#:* <pre>[^a-zA-Z0-9_\s]+</pre>
	#:* <pre>\[a-zA-Z0-9_]*</pre> (LaTeX style token)		#:* <pre>\[a-zA-Z0-9_]+</pre> (LaTeX style token)
	# The translator must check that combination output tokens are not a substring of any input token; this enforces one-pass termination of the translation		# The translator must check that combination output tokens are not a substring of any input token; this enforces one-pass termination of the translation
	# The translator must not process a text token that has the caret over it		# The translator must not process a text token that has the caret over it