Re: [isabelle] RC2: jEdit macros don't work with \<^sub> in them
On 10/11/2013 5:23 AM, Makarius wrote:
I see the text encoding UTF-8-Isabelle here for the bsh file, which is
probably what you mean by "not simple text file".
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.
First, they made significant changes from jEdit 5.0 to jEdit 5.1. I now
have to escape "\" with "\" in a macro, which wasn't the case before.
With Isabelle2013, it also loads a bsh file with UTF-8-Isabelle, but the
macros run fine with Isabelle symbol commands in them.
There are different ways to get a bsh file detected asUTF-8:
However, for me, the safest way with no changes is to put this in a bsh
From past experience with WinEdt, I know I can get deceived about
finding solutions. The encoding that jEdit uses to open a file for the
first time is what it uses after that, unless you explicitly change it,
like with "Utilities/Buffer Options".
If the encoding is specified in the bsh, the macros don't give an error,
but a command like "\<^sub>1" is still not converted graphically like it
is with Isabelle2013.
Behaviour is to some extent accidental, and one needs to change habits
Occasionally, I suppose, but a proper balance requires than one
occasionally, or even frequently, fight for his or her right to party,
as specified in the lyrics of "(You Gotta) Fight for Your Right (To
Party!)", by the Beastie Boys.
I use what's available, and because a Linux version is available, macros
are important enough to be willing to see what that version can do, if
that's what's needed.
Take a relatively simple macro for a set of markup tags like this:
The macro uses && to place me at that spot, and then it's used to get me
out of the tags.
It's not even just the number of escape sequences and tick characters I
have to type. It's remembering what my markup command is, and the fact
that there's about a 70% chance I'll get some part of typing it wrong
It may work to save the file and reload it to get it to it to render the
Thanks for the help,
This archive was generated by a fusion of
Pipermail (Mailman edition) and