This is a side-track of the completion (and tooltip renovation) story.
After many years of struggling with various possibilities for popup
windows in Java/Swing and their many portability problems (evil window
managers etc.), I have recently tried the official
http://docs.oracle.com/javase/7/docs/api/javax/swing/PopupFactory.html
This is a short description as javadoc on the surface, but there are big
and complex sources behind it:
http://www.docjar.com/html/api/javax/swing/PopupFactory.java.html
It seems to workaround various Swing design problems, with lots of
explicit runtime matching of object types. Thus it works a bit better
than plain JWindow, but Apple/Oracle managed to bomb that approach
nonetheless (bad focus, no copy-paste).
The result of studying the sources of javax.swing.PopupFactory to produce
my own version is now this:
http://isabelle.in.tum.de/repos/isabelle/file/31f956f42e8d/src/Tools/jEdit/src/popup.scala
It is hard to tell if this is a joke or if it is funny. The main lesson
learned concerning Java/Swing:
* The smoking chimneys of javax.swing.PopupFactory won't do any good.
* Plain javax.swing.JLayeredPane does all the work.
Lets see if this is really the case -- in everyday use of the new
completion mechanism (and tooltips) on all these exotic platforms.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
