Re: [isabelle] RC2: jEdit macros don't work with \<^sub> in them
On 10/11/2013 5:23 AM, Makarius wrote:
You should probably change that to UTF-8 and make sure that the bsh
script refers to the Unicode character for \<^sub> without anything else.
Using ":encoding=UTF-8:" solved the macro error problem, as I said in
the other email. The second part of your suggestion finally sunk in to
get the macro to insert the subscript rather than insert \<^sub>.
So a macro command like this,
does what " textArea.setSelectedText(\<^isub>^+&&\<^isub>_&&)" was doing
When the bsh file is opened up in another editor, the graphical unicode
characters don't display correctly, but the unicode characters, inserted
by the macro in a THY, get converted to Isabelle commands, such as
\<^sub>, as shown when I open up the THY file in my other editor.
This archive was generated by a fusion of
Pipermail (Mailman edition) and