[isabelle-dev] Facts and semantic completion

Makarius makarius at sketis.net
Tue Mar 18 21:22:11 CET 2014


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



More information about the isabelle-dev mailing list