| Tue, 13 Aug 2013 22:25:24 +0200 | wenzelm | Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java); | changeset | files |
| Tue, 13 Aug 2013 20:35:45 +0200 | wenzelm | merged | changeset | files |
| Tue, 13 Aug 2013 20:34:46 +0200 | wenzelm | discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end; | changeset | files |