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 anymore.

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 already discovered.

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 MHonArc.