Difference between pages "Rodin Keyboard" and "Rodin Platform 1.2 Release Notes"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Nicolas
 
imported>Pascal
 
Line 1: Line 1:
−
The Rodin Keyboard is an extensible keyboard for inputing mathematical formula (in Unicode).  The Rodin keyboard provides the following facilities:
+
{{TOCright}}
−
* 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.
+
== What's New in Rodin 1.2? ==
 +
{{TODO | List here the new features and improvements.}}
  
−
Currently, there are two keyboards available:
+
* [[Generated Model Elements | Generated elements]]
−
* Standard keyboard for Event-B.
 
−
* LaTeX-style keyboard for Event-B.
 
  
−
= Specification =
+
* [[Predicate_variables|Predicate variables extension]]
  
−
== Definitions ==
+
* Migration to Eclipse 3.5 (Galileo)
−
* '''Translator''': function that transforms a ('''source chain''', '''source caret position''') into a ('''target chain''', '''target caret position''')
 
−
* '''Token''': character sequence in a chain that is of one lexical kind, as long as possible
 
−
* '''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)
 
−
 
 
−
== Functional Needs ==
 
−
# Translate a whole chain all at once
 
−
# Translate on the fly, characters being typed in continuously
 
−
# Maintain a coherent caret position
 
−
# Keep spacing unchanged
 
−
# Support statically contributed combinations (add)
 
−
# Support dynamically contributed combinations (check validity, add and remove, will be useful for theories)
 
−
#: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)
 
  
 
== Requirements ==
 
== Requirements ==
 +
* It is recommended to run the Rodin platform with a Java 1.5 Runtime Environment.
 +
* Only a 32-bit version of the Rodin platform is provided. Some optional libraries dedicated to 32-bit support may be required in order to run it on a 64-bit OS. Moreover, you will have to install a 32-bit Java Virtual Machine (JVM), and then to set the -vm option to make sure that Rodin is run with the correct JVM.
 +
:''eg.'' <tt>/usr/local/rodin/rodin -vm /usr/lib/jvm/ia32-java-1.5.0-sun/bin/java</tt> (You have to adjust paths to your system.)
  
−
# The translator must check that combination input tokens are either text or math symbols
+
== External plug-ins ==
−
#: A combination input is a valid text token if it matches <pre>[a-zA-Z0-9_]+</pre> (this excludes 'λ', '$', 'ℙ', … from identifiers)
+
{{TODO | Describe here the available plug-ins, and the supported versions for this release.}}
−
#: A combination input is a valid math token if it matches either:
+
* [[Decomposition_Release_History|Decomposition Plug-in 1.0]]
−
#:* <pre>[^a-zA-Z0-9_\s]+</pre>
 
−
#:* <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 not process a text token that has the caret over it
 
−
# 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, 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)
 
−
 
 
−
== Algorithm ==
 
−
 
 
−
Translation must be performed in the following order:
 
−
# match and translate LaTeX style math tokens (doing it before text tokens, as it may contain translatable text substrings, and before regular math tokens because of first math token '\')
 
−
# match and translate regular math tokens
 
−
# match and translate text tokens
 
−
 
 
−
In order to match, use the above regular expressions for each category.
 
−
Only search for first match, translate, then search for other matches in translated text repeatedly.
 
−
 
 
−
=== 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 'matched', (== original caret position in whole text minus index of 'matched')):
 
−
 
 
−
<pre>
 
−
 
 
−
caretShift = 0 // will be added to the caret position after the translation, to determine new caret position
 
−
pending_translation = false
 
−
 
 
−
attempt = matched
 
−
while(attempt.length() > 0):
 
−
  attempt_has_caret = 0 <= caret <= attempt.length()
 
−
  possible_combinations = find_latex_combinations_with_prefix(attempt)
 
−
 
 
−
  foreach combo in possible_combinations by decreasing length:
 
−
    if combo.length() > attempt.length():
 
−
      if attempt_has_caret:
 
−
        return (translation = matched, pending_translation = true, caretShift = 0)
 
−
      else:
 
−
        // forget this possibility, the user is not typing it
 
−
        possible_combinations.remove(combo)
 
−
        continue
 
−
    if combo.length() == attempt.length(): // actually they are equal then
 
−
      translated_combo = translate(combo)
 
−
      if caret >= combo.length():
 
−
        caretShift += translated_combo.length() - combo.length()
 
−
      return (translation = translated_combo, pending_translation = true, caretShift = caretShift)
 
−
     
 
−
  attempt = remove_last_character(attempt)
 
−
 
 
−
return (translation = matched, pending_translation = false, caretShift = 0)
 
−
 
 
−
</pre>
 
−
 
 
−
=== Math Translation ===
 
−
Translate first longest substrings of matched parts that equal an input combination.
 
−
For instance, given '::=', translate into ':∈=', rather than ':≔'.
 
−
Other examples:
 
−
* '\lambdax' should translate into 'λx'.
 
−
* '\oftypeNAT' should translate into 'NAT' (in a math translation step, but NAT will be processed by text translation)
 
−
 
 
−
If there existed a translation for '/' into '÷' and a translation of '=/=' into '≠' (but no translation for '/=' or any '/*')
 
−
* '=/' with caret should stay unchanged because '=/' potentially starts a combination input, although '/' by itself is the longest combination input starting with '/'
 
−
* '=/' without caret translates to '=÷'
 
−
 
 
−
Given text 'text' to translate and caret position 'caret':
 
−
 
 
−
<pre>
 
−
translation = ""
 
−
caretShift = 0 // will be added to the caret position after the translation, to determine new caret position
 
−
pending_translation = false
 
−
i = 0
 
−
while i <= matched.length() {
 
−
  start_skip = i
 
−
  i = find_math_combination_input_start_skipping_language_symbols(matched,i)
 
  
−
  translation += matched.substring(start_skip, i)
+
== Downloading ==
 +
{{TODO | Add here a link to download the platform.}}
  
−
  if i equals length of matched:
+
== Fixed Bugs ==
−
    return (translation, pending_translation, caretShift)
+
{{TODO | Add here a list of the fixed bugs.}}
  
−
  // i is now at start of a combination input
+
== Known Issues ==
−
  start_combo = i
+
* Early releases of XULRunner 1.9.1 may cause an SWT exception that prevents from opening an editor (as well as any browser-based ui component). More recent releases fix this bug (works fine with xulrunner-1.9.1.7). Alternatively, it is possible to specify XULRunner path to point to 1.9.0: edit "rodin.ini" and add the following line:
−
  i = skip_longest_math_combination_input(matched,i)
+
-Dorg.eclipse.swt.browser.XULRunnerPath=/usr/lib/xulrunner-1.9.0.14
−
 
+
where "/usr/lib/xulrunner-1.9.0.14" must be replaced with your actual XULRunner 1.9.0 install directory.
−
  combo = matched.substring(start_combo, i)
 
  
−
  combo_has_caret = start_combo <= caret <= i
+
* Using Rodin on GNOME desktop may result in a situation where buttons lock windows. To avoid this situation, it is needed to launch Rodin with
 +
GDK_NATIVE_WINDOWS=1 /path_to_rodin/rodin
 +
It's a GTK bug, referenced for Eclipse at [[https://bugs.eclipse.org/bugs/show_bug.cgi?id=291257]]<br />See also [[Gnome and broken buttons]].
  
−
 
+
* A warning like the following one is displayed to the standard output when platform starts on GNOME desktop:
−
  if combo is an incomplete combination input: // combination partially typed in
+
(rodin:17254): GLib-WARNING **: g_set_prgname() called multiple times
−
    if combo_has_caret:
+
It's a GNOME bug. Information found there: [[https://issues.foresightlinux.org/browse/FL-2333]]
−
      pending_translation = true
 
−
      translation += combo
 
−
    else:
 
−
      translation += matched[start_combo]
 
−
      i = start_combo + 1 // rewind and search for combinations inside combo
 
−
    continue
 
  
−
  // now combo is a complete combination input
+
* The error log shows the following problem:
 +
org.osgi.framework.BundleException: The bundle could not be resolved. Reason: Missing Constraint: Import-Package: org.eclipse.equinox.internal.util.event; version="1.0.0"
 +
at org.eclipse.osgi.framework.internal.core.AbstractBundle.getResolverError(AbstractBundle.java:1313)
 +
...
 +
It's an Eclipse 3.5 bug. Information found there: [[http://www.eclipse.org/forums/index.php?t=msg&goto=131264&S=00746ff4ca25d6bd09d287e97ead74ff]]
  
−
  if combo is the longest possible combination input (i.e it is not a prefix of another combination input)
+
* The list of the currently open bugs is given below:
−
    or not combo_has_caret :
+
{{TODO | Add here a link to the SourceForge Bugs page, after filtering bugs (Assignee Any, Status Open, Category Any, Group 1.2).}}
−
    translated_combo = translate(combo)
 
−
    translation += translated_combo
 
−
    if caret >= i:
 
−
      caretShift += translated_combo.length() - combo.length()
 
−
  else:
 
−
    // there exists a longer combination input
 
−
    // and the caret is over the combo: do not translate, let the user the possibility to
 
−
    // type the longer combination input, remember the pending translation status;
 
−
    // when a translation returns with a pending translation status, a caret listener will
 
−
    // be activated, that will trigger a new translation when the caret moves
 
−
    translation += combo
 
−
    pending_translation = true
 
−
   
 
−
</pre>
 
  
−
=== Text Translations ===
+
[[Category:Rodin Platform Release Notes]]
−
Translate whole matched parts that equal an input combination.
 
−
* 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
 
−
[[Category:Design]]
 

Revision as of 10:52, 20 January 2010

What's New in Rodin 1.2?

TODO: List here the new features and improvements.

  • Migration to Eclipse 3.5 (Galileo)

Requirements

  • It is recommended to run the Rodin platform with a Java 1.5 Runtime Environment.
  • Only a 32-bit version of the Rodin platform is provided. Some optional libraries dedicated to 32-bit support may be required in order to run it on a 64-bit OS. Moreover, you will have to install a 32-bit Java Virtual Machine (JVM), and then to set the -vm option to make sure that Rodin is run with the correct JVM.
eg. /usr/local/rodin/rodin -vm /usr/lib/jvm/ia32-java-1.5.0-sun/bin/java (You have to adjust paths to your system.)

External plug-ins

TODO: Describe here the available plug-ins, and the supported versions for this release.

Downloading

TODO: Add here a link to download the platform.

Fixed Bugs

TODO: Add here a list of the fixed bugs.

Known Issues

  • Early releases of XULRunner 1.9.1 may cause an SWT exception that prevents from opening an editor (as well as any browser-based ui component). More recent releases fix this bug (works fine with xulrunner-1.9.1.7). Alternatively, it is possible to specify XULRunner path to point to 1.9.0: edit "rodin.ini" and add the following line:
-Dorg.eclipse.swt.browser.XULRunnerPath=/usr/lib/xulrunner-1.9.0.14

where "/usr/lib/xulrunner-1.9.0.14" must be replaced with your actual XULRunner 1.9.0 install directory.

  • Using Rodin on GNOME desktop may result in a situation where buttons lock windows. To avoid this situation, it is needed to launch Rodin with
GDK_NATIVE_WINDOWS=1 /path_to_rodin/rodin

It's a GTK bug, referenced for Eclipse at [[1]]
See also Gnome and broken buttons.

  • A warning like the following one is displayed to the standard output when platform starts on GNOME desktop:
(rodin:17254): GLib-WARNING **: g_set_prgname() called multiple times

It's a GNOME bug. Information found there: [[2]]

  • The error log shows the following problem:
org.osgi.framework.BundleException: The bundle could not be resolved. Reason: Missing Constraint: Import-Package: org.eclipse.equinox.internal.util.event; version="1.0.0"
at org.eclipse.osgi.framework.internal.core.AbstractBundle.getResolverError(AbstractBundle.java:1313)
...

It's an Eclipse 3.5 bug. Information found there: [[3]]

  • The list of the currently open bugs is given below:

TODO: Add here a link to the SourceForge Bugs page, after filtering bugs (Assignee Any, Status Open, Category Any, Group 1.2).

Retrieved from ‘https://wiki.event-b.org/index.php?title=Rodin_Keyboard&oldid=7364’