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,

textArea.setSelectedText("⇩^+&&⇩_&&");

does what " textArea.setSelectedText(\<^isub>^+&&\<^isub>_&&)" was doing before.

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.

Thanks again,
GB




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.