Email Gateway (Aug 19 2022 at 12:02): Email Gateway (Aug 19 2022 at 12:02):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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
Email Gateway (Aug 19 2022 at 12:02):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Using ":encoding=UTF-8:" solved the macro error problem, as I said in
the other email. The second part of your suggestion finally sunk in to
get the macro to insert the subscript rather than insert \<^sub>.
So a macro command like this,
textArea.setSelectedText("⇩^+&&⇩_&&");
does what " textArea.setSelectedText(\<^isub>^+&&\<^isub>_&&)" was doing
before.
When the bsh file is opened up in another editor, the graphical unicode
characters don't display correctly, but the unicode characters, inserted
by the macro in a THY, get converted to Isabelle commands, such as
\<^sub>, as shown when I open up the THY file in my other editor.
Thanks again,
GB
Email Gateway (Aug 19 2022 at 12:03):From: Gottfried Barrow <gottfried.barrow@gmx.com>
The problem is actually only that the \<^isub> command doesn't exist
anymore. So if I run a macro that tries to use it rather than \<^sub>, I
guess something doesn't get completed correctly by Isabelle/jEdit's
attempt to convert it, and the macro returns an error.
I figured out that a bsh file doesn't need to be UTF-8, and once I let
them be treated as UTF-8-Isabelle again, if I saved a bsh file in jEdit
with a Unicode character for \<^sub>, it would convert the Unicode
character back to \<^sub> just like in a thy file. That and other things
led me to figuring it out.
Here's the error message it returns if there's an attempt to insert
\<^isub> as text:
Sourced file:
E:\E_1\02-p\pi\home\.isabelle\Isabelle2013-1-RC2\jedit\macros\+m..markup3\mu__mft....font_typewriter_primary.bsh
Token Parsing Error: Lexical error at line 6, column 28. Encountered:
"<" (60), after : "\"\\": <at unknown location>
at org.gjt.sp.jedit.bsh.Interpreter.eval(Interpreter.java:698)
at org.gjt.sp.jedit.BeanShell._runScript(BeanShell.java:339)
at org.gjt.sp.jedit.BeanShell._runScript(BeanShell.java:287)
at org.gjt.sp.jedit.BeanShell.runScript(BeanShell.java:213)
at org.gjt.sp.jedit.Macros$BeanShellHandler.runMacro(Macros.java:1151)
at org.gjt.sp.jedit.Macros$Macro.invoke(Macros.java:573)
at
org.gjt.sp.jedit.gui.InputHandler.invokeAction(InputHandler.java:342)
at org.gjt.sp.jedit.jEdit$4.invokeAction(jEdit.java:3423)
at org.gjt.sp.jedit.jEdit$4.invokeAction(jEdit.java:3405)
at
org.gjt.sp.jedit.EditAction$Wrapper.actionPerformed(EditAction.java:212)
at
javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:2018)
at
javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.java:2341)
at
javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:402)
at
javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:259)
at javax.swing.AbstractButton.doClick(AbstractButton.java:376)
at
javax.swing.plaf.basic.BasicMenuItemUI.doClick(BasicMenuItemUI.java:833)
at
javax.swing.plaf.basic.BasicMenuItemUI$Handler.mouseReleased(BasicMenuItemUI.java:877)
at
java.awt.AWTEventMulticaster.mouseReleased(AWTEventMulticaster.java:289)
at java.awt.Component.processMouseEvent(Component.java:6505)
at javax.swing.JComponent.processMouseEvent(JComponent.java:3320)
at java.awt.Component.processEvent(Component.java:6270)
at java.awt.Container.processEvent(Container.java:2229)
at java.awt.Component.dispatchEventImpl(Component.java:4861)
at java.awt.Container.dispatchEventImpl(Container.java:2287)
at java.awt.Component.dispatchEvent(Component.java:4687)
at
java.awt.LightweightDispatcher.retargetMouseEvent(Container.java:4832)
at
java.awt.LightweightDispatcher.processMouseEvent(Container.java:4492)
at java.awt.LightweightDispatcher.dispatchEvent(Container.java:4422)
at java.awt.Container.dispatchEventImpl(Container.java:2273)
at java.awt.Window.dispatchEventImpl(Window.java:2719)
at java.awt.Component.dispatchEvent(Component.java:4687)
at java.awt.EventQueue.dispatchEventImpl(EventQueue.java:735)
at java.awt.EventQueue.access$200(EventQueue.java:103)
at java.awt.EventQueue$3.run(EventQueue.java:694)
at java.awt.EventQueue$3.run(EventQueue.java:692)
at java.security.AccessController.doPrivileged(Native Method)
at
java.security.ProtectionDomain$1.doIntersectionPrivilege(ProtectionDomain.java:76)
at
java.security.ProtectionDomain$1.doIntersectionPrivilege(ProtectionDomain.java:87)
at java.awt.EventQueue$4.run(EventQueue.java:708)
at java.awt.EventQueue$4.run(EventQueue.java:706)
at java.security.AccessController.doPrivileged(Native Method)
at
java.security.ProtectionDomain$1.doIntersectionPrivilege(ProtectionDomain.java:76)
at java.awt.EventQueue.dispatchEvent(EventQueue.java:705)
at
java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:242)
at
java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:161)
at
java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:150)
at
java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:146)
at
java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:138)
at java.awt.EventDispatchThread.run(EventDispatchThread.java:91)
Email Gateway (Aug 19 2022 at 12:04):From: Makarius <makarius@sketis.net>
On Sat, 12 Oct 2013, Gottfried Barrow wrote:
The problem is actually only that the \<^isub> command doesn't exist
anymore.
The technical term for \<^isub> is "control symbol". It still exists but
is uninterpreted, i.e. it looses its former special role as subscript
within identifiers. It also looses its Unicode rendering, as you have
already discovered.
I figured out that a bsh file doesn't need to be UTF-8, and once I let
them be treated as UTF-8-Isabelle again, if I saved a bsh file in jEdit
with a Unicode character for \<^sub>, it would convert the Unicode
character back to \<^sub> just like in a thy file. That and other things
led me to figuring it out.
OK, this sounds like problem solved.
Makarius
Email Gateway (Aug 19 2022 at 12:25):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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.
Regards,
GB
jEdit macro problem.png
Email Gateway (Aug 19 2022 at 12:25):From: Makarius <makarius@sketis.net>
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
Last updated: Nov 21 2024 at 12:39 UTC