proof-unicode-tokens
Table of Contents
- Emacs package
- Proof General
Feature that provides Unicode display/shortcuts.
The implementation of Unicode display seems unnecessarily complicated. If you just want to make certain tokens appear as Unicode characters, it's probably better to just use prettify-symbols-mode.
However, proof-unicode-tokens can do some nifty things that prettify-symbols-mode can't do. In particular, the ability to display arbitrary characters in superscript or subscript is very nice. So it might make sense to use both features, ideally only modifying prettify-symbols-alist.
1. fonts
This feature seems to have been designed back when you couldn't assume that the user's default font would have broad Unicode coverage. As a result, the default behavior is to display special symbols in a different font.
In the modern era, many (most?) popular programming fonts do have broad Unicode coverage. If you use such a font, I recommend at least modifying unicode-tokens-symbol-font-face so that it inherits its family from the default font.
(set-face-attribute 'unicode-tokens-symbol-font-face nil :family 'unspecified)