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:

http://www.jedit.org/users-guide/encodings.html

However, for me, the safest way with no changes is to put this in a bsh file:

// :encoding=UTF-8:

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.

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:

textArea.setSelectedText("\<langle>\<^isub>`+&&\<^isub>`\<rangle>&&");

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 every time.

It may work to save the file and reload it to get it to it to render the symbol commands.

Thanks for the help,
GB




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