tlaplus
Add Unicode Operator completions
This is my first typescript PR ever, so please bear with me if I screwed something up.
The PR has a small bug in it which I couldn't figure out - typing \in<TAB> autocompletes to \∈ and not ∈.
This is already a usability win for me, so I'm hoping someone else can help get this PR across the finish line.
Thanks for the PR! To get it across the finish line, the feature needs to be disabled by default, since not all users want it and not all tools support Unicode characters.
@lemmy Good note, that's been added now.
I'm still not sure of how to get rid of the leading \ slash when doing the autocomplete.
@miguelraz Thanks for the PR! Could you add tests for operator completions? - especially the case where Unicode autocomplete is on but the operator has no mapping?
I'm still not sure of how to get rid of the leading \ slash when doing the autocomplete.
(You've probably thought of this but anyway) from looking at the code it looks like you define the translation without the preceding backslash, like ['E', '∃'], ['A', '∀']; what happens if you define it like ['\\E', '∃'], ['\\A', '∀']?
The full list of supported Unicode symbols can be found here. Given their number I suggest writing a quick script in Python (or similar) ingesting the CSV and spitting out the desired code. Believe me, I've manually written all these out quite a few times and scripting is just so much nicer.
In the TLAUC project it was also found to be useful to skip translating specific groups of symbols, in particular the Nat/Int/Real symbols and also some of the Unicode symbols that are simple contractions of their ASCII counterparts. I don't think this feature is necessary to get the PR in but it would be nice to expose it as a Unicode translation sub-option, some boxes checked by default that if unchecked would skip translating those symbol categories.
- I believe that appending the
\\is handled just a few lines below with the'\\' + w. - Agree on the scripting - did something very similar.
- Yes, I'll be skipping the
Nat/Realfor now because they don't have backslashes, which is my greatest annoyance. - I'm struggling with adding unit tests to be honest. This will take a bit longer because of that.
@miguelraz would it help to have additional usability testing by running this build on my machine, or are the issues basically all known at this point?