tuned proofs;

uniform use of isabelle.jEdit.Popup, based on generic screen location operations;

more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X); observe !evt.isConsumed semantically: no initial dismiss here (e.g. due to cursor keys);