Display keywords as Unicode mathematical symbols

dafny-lang / ide-vscode

VSCode IDE Integration for Dafny

https://marketplace.visualstudio.com/items?itemName=dafny-lang.ide-vscode

MIT License

21 stars 18 forks source link

Display keywords as Unicode mathematical symbols #464

Open alex-chew opened 3 months ago

alex-chew commented 3 months ago

Dafny users can have Emacs display certain keywords as Unicode mathematical symbols, like ∀ for forall: https://github.com/boogie-org/boogie-friends

It would be nice for the VSCode IDE to support this too.

MikaelMayer commented 3 months ago

I remember that we started to drop support for unicode mathematical symbols as Dafny is not targeted towards mathematicians but more engineers who are usually not used to typing and reading mathematical symbols in their code.

kjx commented 1 month ago

for what it's worth, I strongly suggest we don't do this. Having "intense discussions" with Andrew Black over this regarding Grace, I think expecting normal humans to write programs using characters that are not visible on their keyboards "will not help [adoption"... zx81-keyboard Space-cadet

alex-chew commented 1 month ago

In case I wasn't clear in my original comment, I wasn't suggesting that an option to display some keywords as Unicode symbols should be enabled by default.

kjx commented 1 month ago

that's fine. this is really just an excuse to post in pictures of daft keyboards.

now: export to LaTeX - that's a different matter...