[isabelle-dev] Facts and semantic completion

[Makarius]

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