[isabelle] (Isabelle/)jEdit exception



Hallo,

I noticed a strange error when doing search/replace with
(Isabelle/)jEdit. The error seems to occur no matter what document is
open, even in normal text mode.

To reproduce, search/replace any non-empty string with a string that
starts or ends with a full stop (".") character. I attached the stack
trace. My hg id is e367b93f78e5; I haven't tested it with any other
Isabelle versions because I have none installed.


Cheers,

Manuel
Parse error at line 3, column 9.  Encountered: .
	at org.gjt.sp.jedit.bsh.Parser.generateParseException(Parser.java:5806)
	at org.gjt.sp.jedit.bsh.Parser.jj_consume_token(Parser.java:5758)
	at org.gjt.sp.jedit.bsh.Parser.Expression(Parser.java:1046)
	at org.gjt.sp.jedit.bsh.Parser.PrimaryPrefix(Parser.java:2098)
	at org.gjt.sp.jedit.bsh.Parser.PrimaryExpression(Parser.java:2017)
	at org.gjt.sp.jedit.bsh.Parser.PostfixExpression(Parser.java:1954)
	at org.gjt.sp.jedit.bsh.Parser.UnaryExpressionNotPlusMinus(Parser.java:1839)
	at org.gjt.sp.jedit.bsh.Parser.UnaryExpression(Parser.java:1732)
	at org.gjt.sp.jedit.bsh.Parser.MultiplicativeExpression(Parser.java:1627)
	at org.gjt.sp.jedit.bsh.Parser.AdditiveExpression(Parser.java:1584)
	at org.gjt.sp.jedit.bsh.Parser.ShiftExpression(Parser.java:1525)
	at org.gjt.sp.jedit.bsh.Parser.RelationalExpression(Parser.java:1458)
	at org.gjt.sp.jedit.bsh.Parser.InstanceOfExpression(Parser.java:1430)
	at org.gjt.sp.jedit.bsh.Parser.EqualityExpression(Parser.java:1387)
	at org.gjt.sp.jedit.bsh.Parser.AndExpression(Parser.java:1344)
	at org.gjt.sp.jedit.bsh.Parser.ExclusiveOrExpression(Parser.java:1312)
	at org.gjt.sp.jedit.bsh.Parser.InclusiveOrExpression(Parser.java:1269)
	at org.gjt.sp.jedit.bsh.Parser.ConditionalAndExpression(Parser.java:1226)
	at org.gjt.sp.jedit.bsh.Parser.ConditionalOrExpression(Parser.java:1183)
	at org.gjt.sp.jedit.bsh.Parser.ConditionalExpression(Parser.java:1143)
	at org.gjt.sp.jedit.bsh.Parser.Expression(Parser.java:1043)
	at org.gjt.sp.jedit.bsh.Parser.ReturnStatement(Parser.java:3421)
	at org.gjt.sp.jedit.bsh.Parser.Statement(Parser.java:2633)
	at org.gjt.sp.jedit.bsh.Parser.BlockStatement(Parser.java:2710)
	at org.gjt.sp.jedit.bsh.Parser.Block(Parser.java:2674)
	at org.gjt.sp.jedit.bsh.Parser.MethodDeclaration(Parser.java:354)
	at org.gjt.sp.jedit.bsh.Parser.BlockStatement(Parser.java:2705)
	at org.gjt.sp.jedit.bsh.Parser.Line(Parser.java:145)
	at org.gjt.sp.jedit.bsh.Interpreter.Line(Interpreter.java:998)
	at org.gjt.sp.jedit.bsh.Interpreter.eval(Interpreter.java:634)
	at org.gjt.sp.jedit.bsh.Interpreter.eval(Interpreter.java:738)
	at org.gjt.sp.jedit.bsh.Interpreter.eval(Interpreter.java:727)
	at org.gjt.sp.jedit.BeanShellFacade._eval(BeanShellFacade.java:148)
	at org.gjt.sp.jedit.BeanShellFacade.cacheBlock(BeanShellFacade.java:190)
	at org.gjt.sp.jedit.BeanShell.cacheBlock(BeanShell.java:414)
	at org.gjt.sp.jedit.search.SearchAndReplace.initReplace(SearchAndReplace.java:1082)
	at org.gjt.sp.jedit.search.SearchAndReplace.replaceAll(SearchAndReplace.java:893)
	at org.gjt.sp.jedit.search.SearchAndReplace.replaceAll(SearchAndReplace.java:855)
	at org.gjt.sp.jedit.search.SearchDialog$ButtonActionHandler.actionPerformed(SearchDialog.java:1124)
	at javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:2022)
	at javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.java:2348)
	at javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:402)
	at javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:259)
	at javax.swing.plaf.basic.BasicButtonListener.mouseReleased(BasicButtonListener.java:252)
	at java.awt.Component.processMouseEvent(Component.java:6535)
	at javax.swing.JComponent.processMouseEvent(JComponent.java:3324)
	at java.awt.Component.processEvent(Component.java:6300)
	at java.awt.Container.processEvent(Container.java:2236)
	at java.awt.Component.dispatchEventImpl(Component.java:4891)
	at java.awt.Container.dispatchEventImpl(Container.java:2294)
	at java.awt.Component.dispatchEvent(Component.java:4713)
	at java.awt.LightweightDispatcher.retargetMouseEvent(Container.java:4888)
	at java.awt.LightweightDispatcher.processMouseEvent(Container.java:4525)
	at java.awt.LightweightDispatcher.dispatchEvent(Container.java:4466)
	at java.awt.Container.dispatchEventImpl(Container.java:2280)
	at java.awt.Window.dispatchEventImpl(Window.java:2750)
	at java.awt.Component.dispatchEvent(Component.java:4713)
	at java.awt.EventQueue.dispatchEventImpl(EventQueue.java:758)
	at java.awt.EventQueue.access$500(EventQueue.java:97)
	at java.awt.EventQueue$3.run(EventQueue.java:709)
	at java.awt.EventQueue$3.run(EventQueue.java:703)
	at java.security.AccessController.doPrivileged(Native Method)
	at java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:76)
	at java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:86)
	at java.awt.EventQueue$4.run(EventQueue.java:731)
	at java.awt.EventQueue$4.run(EventQueue.java:729)
	at java.security.AccessController.doPrivileged(Native Method)
	at java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:76)
	at java.awt.EventQueue.dispatchEvent(EventQueue.java:728)
	at java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:201)
	at java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:116)
	at java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:105)
	at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)
	at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:93)
	at java.awt.EventDispatchThread.run(EventDispatchThread.java:82)



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