I'm using Windows.jEdit is not treating .bsh files as simple text files, which causes my macros to return an error and not work like they did in Isabelle2013.
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");Before exiting jEdit, I can run that macro in a THY file and it doesn't cause an error, though the inserted text shows \<^sub>1 rather than a subscripted 1 like it should. Also, before exiting, the text in test.bsh is displayed as ASCII text like it should be.
When I exit jEdit and start it back up, the macro, when run, now causes a Beanshell error. Also, in the window where test.bsh is viewed, jEdit now displays \<^sub> as a graphical bar.
I attach a screenshot showing how jEdit is not displaying only ASCII text in test.bsh.
jEdit macro problem.png
Description: PNG image