ahelwer
commented
1 year ago ---- MODULE Test ----
CurrentDiamondOperator == □⋄P
NewWhiteDiamond == □◇P
TestHandleParseError == 1 + 2 + 3
====Here's a test of how the operator looks. Since the diamond operator is often used next to the box operator, it actually makes sense that they would be drawn from the same unicode block. I think the proposed new white diamond operator looks quite a bit nicer. The TLA+ tree-sitter grammar highlighting used by github fails to highlight it right now of course (since it's invalid syntax), but it seems to recover from the parse error fairly well. I propose changing the diamond operator to ◇ White Diamond (U+25C7) Geometric Shapes Block. Work necessary:
- [x] Update the unicode csv file in this repo and add a statement to the README logging the change
- [x] Update tree-sitter-tlaplus to accept the new operator (might as well keep accepting the old one for backward compatibility)
- [x] Email github team to update the tree-sitter-tlaplus version used for highlighting on github (this has become quite out of date by now, last time I asked them to do this a year ago they never got around to it)
- [x] Update tlauc to convert ASCII to new diamond symbol
- [x] Update TLA+ neovim plugin to auto-translate
<>to new diamond symbol
lemmy
The current diamond operator shows up quite small in some cases (VS Code in macOS, see https://github.com/tlaplus-community/tlauc/issues/4). Currently we use:
⋄ Diamond Operator (U+22C4) Mathematical Operators Block
Here are some alternatives:
The diamond operator (current standard) is semantically the most appropriate, as it is included in the mathematical operators block. The specific font used in VS Code in macOS certainly displays it weirdly (some would say incorrectly). The White Diamond symbol of the Geometric Shapes Block is probably the most appropriate alternative. Note the
[]operator is currently □ White Square (U+25A1) Geometric Shapes Block (no equivalent exists in the Mathematical Symbols Block weirdly) so this is not without precedent.