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



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)





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