Re: [isabelle] RC2: jEdit macros don't work with \<^sub> in them



On Thu, 10 Oct 2013, Gottfried Barrow wrote:

jEdit is not treating .bsh files as simple text files

For a test case, I record a simple macro while in jEdit, and save it to test.bsh, the contents which is this:

textArea.setSelectedText("\\<^sub>1");

I attach a screenshot showing how jEdit is not displaying only ASCII text in test.bsh.

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.

Generally, "simple text" and "Unicode" are in conflict, and there are always surprises to be expected.


I can't say where the change of behaviour is coming from. Isabelle2013 was composed of many contributing components, and Isabelle2013-1 of many slightly different ones, and some genuine changes on our side.

Behaviour is to some extent accidental, and one needs to change habits occasionally.


	Makarius




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