| Sun, 25 Aug 2013 13:59:40 +0200 | wenzelm | use view root as parent for popup, which provides more space and avoids confusion of mouse wheel handlers on Windows (wrt. text area scrollbar); | changeset | files |
| Sat, 24 Aug 2013 23:16:37 +0200 | wenzelm | tuned proofs; | changeset | files |
| Sat, 24 Aug 2013 21:23:40 +0200 | wenzelm | tuned proofs; | changeset | files |
| Sat, 24 Aug 2013 18:29:23 +0200 | wenzelm | confine popup to parent component, to avoid javax.swing.PopupFactory$HeavyWeightPopup and its problems with Linux window management and Mac OS X key handling; | changeset | files |