Re: [isabelle] RC2: jEdit macros don't work with \<^sub> in them
On Sat, 12 Oct 2013, Gottfried Barrow wrote:
The problem is actually only that the \<^isub> command doesn't exist
The technical term for \<^isub> is "control symbol". It still exists but
is uninterpreted, i.e. it looses its former special role as subscript
within identifiers. It also looses its Unicode rendering, as you have
I figured out that a bsh file doesn't need to be UTF-8, and once I let
them be treated as UTF-8-Isabelle again, if I saved a bsh file in jEdit
with a Unicode character for \<^sub>, it would convert the Unicode
character back to \<^sub> just like in a thy file. That and other things
led me to figuring it out.
OK, this sounds like problem solved.
This archive was generated by a fusion of
Pipermail (Mailman edition) and