Re: [isabelle] Isabelle2014-RC0 available for testing



> When I start jEdit and quickly open the menu (I usually first go to File
> → Recently used files), a moment later something happens that seems to
> give focus to the main window, while the menu is still open. This means
> that I cannot click on the open menu any more (and hover has no effect)
> and I first have to close the menu and re-open it.

I can confirm that, using Linux (with KDE as desktop environment). It
doesn't happen with 2013-2.

Opening the menu right after jEdit opens also produces a stack trace:

1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0: Exception in
thread "AWT-EventQueue-0"
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:
java.lang.NullPointerException
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
org.gjt.sp.jedit.jEdit$4.invokeAction(jEdit.java:3414)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
org.gjt.sp.jedit.jEdit$4.invokeAction(jEdit.java:3405)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
org.gjt.sp.jedit.EditAction$Wrapper.actionPerformed(EditAction.java:212)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:2018)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.java:2341)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:402)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:259)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
javax.swing.AbstractButton.doClick(AbstractButton.java:376)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
javax.swing.AbstractButton.doClick(AbstractButton.java:356)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
javax.swing.plaf.basic.BasicPopupMenuUI$BasicMenuKeyListener.menuKeyPressed(BasicPopupMenuUI.java:358)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
javax.swing.JPopupMenu.fireMenuKeyPressed(JPopupMenu.java:1417)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
javax.swing.JPopupMenu.processMenuKeyEvent(JPopupMenu.java:1396)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
javax.swing.JPopupMenu.processKeyEvent(JPopupMenu.java:1380)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
javax.swing.MenuSelectionManager.processKeyEvent(MenuSelectionManager.java:455)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
javax.swing.plaf.basic.BasicPopupMenuUI$MenuKeyboardHelper.keyPressed(BasicPopupMenuUI.java:1200)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.Component.processKeyEvent(Component.java:6474)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
javax.swing.JComponent.processKeyEvent(JComponent.java:2828)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.Component.processEvent(Component.java:6293)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.Container.processEvent(Container.java:2229)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.Component.dispatchEventImpl(Component.java:4872)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.Container.dispatchEventImpl(Container.java:2287)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.Component.dispatchEvent(Component.java:4698)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.KeyboardFocusManager.redispatchEvent(KeyboardFocusManager.java:1887)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.DefaultKeyboardFocusManager.dispatchKeyEvent(DefaultKeyboardFocusManager.java:762)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.DefaultKeyboardFocusManager.preDispatchKeyEvent(DefaultKeyboardFocusManager.java:1027)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.DefaultKeyboardFocusManager.typeAheadAssertions(DefaultKeyboardFocusManager.java:899)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.DefaultKeyboardFocusManager.dispatchEvent(DefaultKeyboardFocusManager.java:727)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.Component.dispatchEventImpl(Component.java:4742)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.Container.dispatchEventImpl(Container.java:2287)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.Window.dispatchEventImpl(Window.java:2719)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.Component.dispatchEvent(Component.java:4698)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.EventQueue.dispatchEventImpl(EventQueue.java:735)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.EventQueue.access$200(EventQueue.java:103)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.EventQueue$3.run(EventQueue.java:694)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.EventQueue$3.run(EventQueue.java:692)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.security.AccessController.doPrivileged(Native Method)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.security.ProtectionDomain$1.doIntersectionPrivilege(ProtectionDomain.java:76)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.security.ProtectionDomain$1.doIntersectionPrivilege(ProtectionDomain.java:87)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.EventQueue$4.run(EventQueue.java:708)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.EventQueue$4.run(EventQueue.java:706)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.security.AccessController.doPrivileged(Native Method)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.security.ProtectionDomain$1.doIntersectionPrivilege(ProtectionDomain.java:76)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.EventQueue.dispatchEvent(EventQueue.java:705)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:242)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:161)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:150)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:146)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:138)
1:15:37 PM [AWT-EventQueue-0] [error] AWT-EventQueue-0:  at
java.awt.EventDispatchThread.run(EventDispatchThread.java:91)





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