Email Gateway (Oct 01 2026 at 20:30): Email Gateway (Oct 01 2026 at 20:30):From: Benoît Ballenghien <docteur.benoit.ballenghien@gmail.com>
Dear all,
I've noticed a small issue with command+hovering in the Output panel.
For instance, consider a free variable f :: 'a ⇒ 'a. When hovering over f in the theory editor, the popup correctly displays:
free variable
:: 'a ⇒ 'a
However, when doing the same in the Output panel, the popup displays:
language: term
free variable
command.term: fixed "f"
:: 'a \<Rightarrow> 'a
It seems that Isabelle symbols are not properly pretty-printed in the latter case (the issue is not specific to \<Rightarrow>).
Best,
Benoît
Email Gateway (Oct 05 2026 at 21:39):From: Makarius <makarius@sketis.net>
On 01/10/2026 22:29, Benoît Ballenghien wrote:
However, when doing the same in the Output panel, the popup displays:
|language: term free variable command.term: fixed "f" :: 'a \<Rightarrow> 'a |
It seems that Isabelle symbols are not properly pretty-printed in the latter
case (the issue is not specific to |\<Rightarrow>|).
I have addressed that in Isabelle2026-RC3: it was a confusion of the
underlying buffer encoding.
Isabelle2026 is generally more accurate in observing the encoding given by the
user: UTF-8-Isabelle for decoded Isabelle symbols, and UTF-8 for the original
plain text. This is vital for accessibility: \<Rightarrow> is easy to read on
a Braille display, but Unicode characters are not pretty at all.
Makarius
Last updated: Oct 08 2026 at 21:07 UTC