Direct display of symbols

[Alexander-N]

Thank you for this great extension, for me it really makes a huge difference when working with TLA+!

One advantage compared to the TLA Toolbox is that it's possible to configure VSCode so that the mathematical symbols are directly displayed, which I find much easier to read. There is vsc-conceal which can be used with the settings from this PR. Since I found the unicode characters a bit small I use it together with FiraCode which gives results like this:

before

after

I was wondering what others think of this, maybe there are more/better ways to get similar results? Is this worth documenting in the wiki? The settings I used are in this gist.

[alygin]

@Alexander-N, thanks for bringing up an interesting subject.

VSC-Conceal looks cool and it really works best in conjunction with Fira Code. I agree that it's worth mentioning in the wiki, I'll get back to it soon.

I myself prefer narrow fonts and use Pragmata Pro with ligatures that cover many substitutions mentioned in your vsc-conceal config. Unfortunately, not all unicode symbols that represent math operators are displayed as good as in Fira Code, so I switched them off. Actually, I only left few vsc-conceal substitutions for TLA+, but they work fine for me.

[Alexander-N]

The goal of my settings was to use substitutions to unicode only for the cases which are not covered by FiraCode.

So for example in the linked PR there was

{
  "ugly": "#|/=",
  "pretty": "≠"
}

which I changed so that it matches the ligature for "not equal" by FiraCode:

{
  "ugly": "#|/=",
  "pretty": "!="
}

[alygin]

I've added a page to the Wiki with this information.

[lemmy]

I haven't looked into it, but the wiki page should perhaps warn about potential problems outlined in https://www.reddit.com/r/tlaplus/comments/njmjwd/on_mathematical_notation/gzmikod

[Alexander-N]

For me it's more like an additional unimplemented feature than a problem.