Skip to content

add ligatures for tla+ (dk01 feature)#1645

Closed
davidkern wants to merge 1 commit intotonsky:masterfrom
davidkern:liga-tla-plus
Closed

add ligatures for tla+ (dk01 feature)#1645
davidkern wants to merge 1 commit intotonsky:masterfrom
davidkern:liga-tla-plus

Conversation

@davidkern
Copy link
Copy Markdown

@davidkern davidkern commented Apr 10, 2025

Adds ligatures for TLA+ (see: https://mbt.informal.systems/docs/tla_basics_tutorials/tla+cheatsheet.html)

Handles all of the set operations, but not yet \o and \X.
I'm unsure how to add ringoperator (0x2218) to the glyph set.

To use this with vscode. Install deps and build according to the README, and then add these settings:

    "editor.fontFamily": "'Fira Code'",
    "editor.fontLigatures": "'cv24', 'dk01'"

The 'cv24' feature handles /=.

@tonsky
Copy link
Copy Markdown
Owner

tonsky commented Apr 10, 2025

In Fira Code, we keep width of the characters we replace. That was one of the main principles.

Also, what is dk01?

@davidkern
Copy link
Copy Markdown
Author

davidkern commented Apr 10, 2025

Oh, no - I meant to open this as a PR against my own fork as I played with this. Sorry for actually submitting this upstream to you! (dk01 was so I didn't conflict with anything in my branch).

TLA+ is weird, it uses some LaTeX markup for some of its operations - so having \union and \intersect respect their original length would look pretty strange. So this probably wouldn't make sense to ever upstream?

How can I add missing glyphs? I noticed \u2218 renders the ∘ symbol fine, but I couldn't figure out how to define it in the glyphs file so I can sub to it.

We can close this PR out and I'll be more careful with github! Thanks for the excellent work.

@tonsky tonsky closed this Apr 10, 2025
@alexeyten
Copy link
Copy Markdown

@davidkern Just for information, Microsoft recommends to use four uppercase letters for private features.
https://learn.microsoft.com/en-gb/typography/opentype/spec/featuretags

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants