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:
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and