Mario Xerxes Castelán Castro (Jan 10 2026 at 01:45): Mario Xerxes Castelán Castro (Jan 10 2026 at 01:45):Will Isabelle work if are stored as the character they are displayed as, instead of using the Isabelle-specific encoding? I know this is handled by the encoding which is UTF-8-Isabelle. I noticed the completion menu does not pop up when using encoding UTF-8.
Kevin Kappelmann (Jan 10 2026 at 10:45):It will lead to strange behaviours, e.g. Isabelle/jEdit might not complain. but isabelle build will fail.
See this thread #Beginner Questions > Github
Qiyuan Xu (Jan 12 2026 at 16:25):My REPL supports the conversion between Isabelle's ASCII encoding and Unicode. It reads the system and the user symbol file to parse the ASCII symbols, so almost identical to how the system handles it.
Fabian Huch (Jan 13 2026 at 14:05):Note on this topic: While there are UTF-8 codepoints for many Isabelle symbols (not for all), converting to UTF-8 only makes sense in specific contexts. For instance, \<^sup> has the unicode codepoint ⇧, but you really want to display the following symbol in superscript instead, unless you're e.g. directly editing the identifier that contains ⇧.
Fabian Huch (Jan 13 2026 at 14:06):And UTF-8 characters don't generally exist for superscipted/subscripted characters.
Mario Xerxes Castelán Castro (Jan 13 2026 at 23:38):Fabian Huch ha dicho:
And UTF-8 characters don't generally exist for superscipted/subscripted characters.
Of course, but UTF-8 has subcripts and superscripts for digits, which is the most common use of subscripts and superscripts.
Fabian Huch (Jan 14 2026 at 08:44):Certainly not in general math -- that should be obvious, but you can just look into the AFP: list of ⇧ usage (within the first three hits, you will find characters not representable by UTF-8, and you'll have to scroll far to find numbers).
The whole reason why UTF-8 does not support arbitrary superscript/subscript is that it is not meant for rich text representation, in particular not for mathematical formulae (proposals to add more sub/superscript characters were dismissed by the consortium for this exact reason).
Fabian Huch (Jan 14 2026 at 08:46):Another issue, when talking symbols more generally, is that having a symbol encoding is not good enough. There are plenty of superscript symbols that exist in UTF-8, but your font won't actually be able to render them. Let alone the font of some other user. And even if rendered at all, the symbol might be represented differently...
Fabian Huch (Jan 14 2026 at 08:48):The idea (which I have heard from people using other ITPs) that monospaced UTF-8 would be good enough for math seems crazy to me.
Mario Xerxes Castelán Castro (Jan 15 2026 at 01:13):I understand having a general notation that is not dependent on non-ASCII Unicode support. Nonetheless, Isabelle should use the existing Unicode characters for logical connectives like ∀, ∃, etc. All serious programming fonts include these characters.
Fabian Huch (Jan 15 2026 at 08:33):I don't really see how you can demand that it 'should' do that, when unicode is neither sufficient nor necessary here. In any case, monospaced programming fonts are not adequate at all for displaying logical connectives such as a long implication arrow -- you get a tiny => instead of the proper ==> . Not to mention large operators such as a sum sign...
Fabian Huch (Jan 15 2026 at 08:35):In Isabelle we favor great technology over popular solutions. Use a different ITP if you want the latter, e.g. Lean.
Mario Xerxes Castelán Castro (Jan 16 2026 at 02:40):Fabian Huch ha dicho:
In Isabelle we favor great technology over popular solutions. Use a different ITP if you want the latter, e.g. Lean.
I like that philosophy and I chose Isabelle over Lean for that reason among others. I mean using Unicode characters for symbols that already exist in Unicode, not to change Isabelle to only use such symbols. The reason is so that when one sees theory files using tools other than Isabelle/jEdit, such symbols will be displayed properly. It is better to see ¬ (∀x. P x) instead of \<not> (\<forall>x. P x). In the case of ==>, Unicode has ⟹ U+27F9 LONG RIGHTWARDS DOUBLE ARROW. Note it displays longer than ⇒ in Zulip.
Last updated: Jan 16 2026 at 08:33 UTC