Toolbox beta release with Unicode support

[Markus Alexander Kuppe]

Hi all,

Ron Pressler contributed Unicode support to the TLAToolbox. Unicode support makes it possible to render TLA+ with Unicode characters. We believe Unicode support to improve readability especially for new users due to the more familiar syntax.

Unicode support works for all Toolbox windows: the TLA+ editor, the Model Editor and the Error Trace. See the screenshot below which show the TLA+ editor and the Error Trace with Unicode support enabled. Unicode support works at the UI level only and can be easily toggled via the File> "Use Unicode" menu entry. Your .tla files do not get rewritten with Unicode characters. When typing with Unicode support enabled, ASCII input is converted to Unicode on-the-fly. You do not have to type Unicode.

   

The Unicode support required significant changes in the Toolbox code base and although the feature appears solid, we think it is best to initially release a beta version. Once we will have gathered sufficient feedback from the beta testers, we will incorporate Unicode support into the regular Toolbox release. This is why the download link at https://tla2.msr-inria.inria.fr/unicode/ wants you to enter an email address with which we might eventually solicit feedback. We will not use your email address for any other purpose.

Thanks,

Markus

[Christian Spann]

Hi,

looks like a great feature.

A first feedback from me:
- I had to increase font size from 9 to 16 pt to get windows to render the Unicode chars nicely on my lenovo t450s.
- Unicode is not rendered correctly inside /* comments which makes commented code unreadable as the parser detects the characters and changes them to ? boxes. I suppose the intention is that comments should either be parsed correctly or not all what ever seems to be more intuitive. I would prefer the first option.

Best regards,
Christian

Am 15.08.2017 um 20:04 schrieb Markus Alexander Kuppe:
>
> Hi all,
>
> Ron Pressler contributed Unicode support to the TLAToolbox. Unicode support makes it possible to render TLA+ with Unicode characters. We believe Unicode support to improve readability especially for new users due to the more familiar syntax.
>
> Unicode support works for all Toolbox windows: the TLA+ editor, the Model Editor and the Error Trace. See the screenshot below which show the TLA+ editor and the Error Trace with Unicode support enabled. Unicode support works at the UI level only and can be easily toggled via the File> "Use Unicode" menu entry. Your .tla files do not get rewritten with Unicode characters. When typing with Unicode support enabled, ASCII input is converted to Unicode on-the-fly. You do not have to type Unicode.
>
>

> The Unicode support required significant changes in the Toolbox code base and although the feature appears solid, we think it is best to initially release a beta version. Once we will have gathered sufficient feedback from the beta testers, we will incorporate Unicode support into the regular Toolbox release. This is why the download link at https://tla2.msr-inria.inria.fr/unicode/ wants you to enter an email address with which we might eventually solicit feedback. We will not use your email address for any other purpose.
>
> Thanks,
>
> Markus
>

> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com <mailto:tlaplus+u...@googlegroups.com>.
> To post to this group, send email to tla...@googlegroups.com <mailto:tla...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

--
Christian Spann
Teamleiter Frontend Services

kiz - Universität Ulm
Abteilung Infrastruktur

Raum O26 5206
Tel. +49 731 50 22484

Diese E-Mail ist digital unterschrieben, weshalb Sie sich sicher sein können dass sie von mir stammt. Mehr dazu hier <https://www.uni-ulm.de/einrichtungen/kiz/service-katalog/it-sicherheit/digitale-zertifikate/dfn-global-zertifikate/>.

[Christian Spann]

Hi,

looks like a great feature.

A first feedback from me:
- I had to increase font size from 9 to 16 pt to get windows to render the Unicode chars nicely on my lenovo t450s.
- Unicode is not rendered correctly inside /* comments which makes commented code unreadable as the parser detects the characters and changes them to ? boxes. I suppose the intention is that comments should either be parsed correctly or not all what ever seems to be more intuitive. I would prefer the first option.

Best regards,
Christian

Am 15.08.2017 um 20:04 schrieb Markus Alexander Kuppe:
>

> Hi all,
>
> Ron Pressler contributed Unicode support to the TLAToolbox. Unicode support makes it possible to render TLA+ with Unicode characters. We believe Unicode support to improve readability especially for new users due to the more familiar syntax.
>
> Unicode support works for all Toolbox windows: the TLA+ editor, the Model Editor and the Error Trace. See the screenshot below which show the TLA+ editor and the Error Trace with Unicode support enabled. Unicode support works at the UI level only and can be easily toggled via the File> "Use Unicode" menu entry. Your .tla files do not get rewritten with Unicode characters. When typing with Unicode support enabled, ASCII input is converted to Unicode on-the-fly. You do not have to type Unicode.
>
>

> The Unicode support required significant changes in the Toolbox code base and although the feature appears solid, we think it is best to initially release a beta version. Once we will have gathered sufficient feedback from the beta testers, we will incorporate Unicode support into the regular Toolbox release. This is why the download link at https://tla2.msr-inria.inria.fr/unicode/ wants you to enter an email address with which we might eventually solicit feedback. We will not use your email address for any other purpose.
>
> Thanks,
>
> Markus
>

[Markus Alexander Kuppe]

On 23.08.2017 17:17, Christian Spann wrote:
> Unicode is not rendered correctly inside /* comments which makes
> commented code unreadable as the parser detects the characters and
> changes them to ? boxes. I suppose the intention is that comments
> should either be parsed correctly or not all what ever seems to be
> more intuitive. I would prefer the first option.

Hi Christian,

I looked into this today and unfortunately I failed to reproduce your
issue on either Windows or Linux. The Toolbox correctly converts ASCII
to Unicode even in single-line comments ("\*"), e.g. see the attached
screenshot.

Let me know if I'm misreading your description of the bug.

Thanks

Markus

[gabri...@gmail.com]

On Tuesday, August 15, 2017 at 3:05:00 PM UTC-3, Markus Alexander Kuppe wrote:
> Hi all,
>
> Ron Pressler contributed Unicode support to the TLAToolbox.
> Unicode support makes it possible to render TLA+ with Unicode
> characters. We believe Unicode support to improve readability
> especially for new users due to the more familiar syntax.
>
> Unicode support works for all Toolbox windows: the TLA+ editor,
> the Model Editor and the Error Trace. See the screenshot below
> which show the TLA+ editor and the Error Trace with Unicode
> support enabled. Unicode support works at the UI level only and
> can be easily toggled via the File> "Use Unicode" menu entry.
> Your .tla files do not get rewritten with Unicode characters. When
> typing with Unicode support enabled, ASCII input is converted to
> Unicode on-the-fly. You do not have to type Unicode.
>
>
>    
>
>

> The Unicode support required significant changes in the Toolbox
> code base and although the feature appears solid, we think it is
> best to initially release a beta version. Once we will have
> gathered sufficient feedback from the beta testers, we will
> incorporate Unicode support into the regular Toolbox release. This
> is why the download link at https://tla2.msr-inria.inria.fr/unicode/
> wants you to enter an email address with which we might eventually
> solicit feedback. We will not use your email address for any other
> purpose.
> Thanks,
>
> Markus

With the intention of just give some feedback on this I'd like to note that I miss Unicode support in the last toolbox release (i.e. 1.5.6)

[Markus Kuppe]

On 19.03.2018 21:56, gabri...@gmail.com wrote:
> With the intention of just give some feedback on this I'd like to note that I miss Unicode support in the last toolbox release (i.e. 1.5.6)

Hi Gabriel,

Unicode supported introduced regressions in the Toolbox which is why we
reverted it [1].

Thanks

Markus

[1] https://github.com/tlaplus/tlaplus/issues/64

[gabri...@gmail.com]

On Tuesday, March 20, 2018 at 9:12:10 AM UTC-3, Markus Alexander Kuppe wrote:

> On 19.03.2018 21:56, gabriel wrote:
> > With the intention of just give some feedback on this I'd like to note that I miss Unicode support in the last toolbox release (i.e. 1.5.6)
>
> Hi Gabriel,
>
> Unicode supported introduced regressions in the Toolbox which is why we
> reverted it [1].
>
> Thanks
>
> Markus
>
> [1] https://github.com/tlaplus/tlaplus/issues/64

oh, I definitely missed that issue. Thanks!

Gabriel