Ligature Boundaries #21340
Description
The Problem:
The Solution:
Probably something like this: https://forum.glyphsapp.com/t/advice-for-discretionary-ligatures/20983
Except instead of @AllLetters, create custom glyph classes based on Rocq's tokenization (which I don't personally know the details of). For the letter-ended ligatures (False L·L True forall l·l), this would probably be identifier characters (something like alphanumeric + _ + '), while for the symbolic ligatures (:= :> -> /\ \/ => <-> <=> <-) this would probably be certain symbol characters. Generally, whichever characters continue the same token rather than starting a new one.
Remember to include two ignore rules per ligature, one for the preceding character and one for the subsequent character (not a single rule that wraps the ligature on both sides), e.g. do:
ignore sub @IdentChar f' o' r' a' l' l';
ignore sub f' o' r' a' l' l' @IdentChar;
Depending on Rocq's tokenization rules, the two ignore rules could use different classes, but this seems unlikely.
EDIT: The deployed fonts used to render these webpages are the "SourceCode" fonts at: https://github.com/rocq-prover/rocq-prover.org/tree/main/asset/vendors/font-files (modified from the originals to add the aforementioned ligatures).