On Fri, 14 Mar 2014, Makarius wrote:
The machanics of the GUI popup are still that of last summer, but that
is a different story.
I have changed that now in Isabelle/416f7a00e4cb.
The regular jEdit completion popup (for word completion from the text)
uses some slightly odd tricks that were once part of my popup, but then I
had removed them in favour of normal GUI focus policies. That turned out
the problem last summer: too many GUI components opening and closing too
quickly lead to key events falling into nothingness.
Now the "KeyEventInterceptor" being back, in a slightly different costume
than before, so it might actually work. The trick here is that the popup
does not change the focus at all, but it "intercepts" events sent to the
main text area. Funnily, the jEdit version of that trick has both focus
and interception, just to add to the confusion.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
