Sat, 15 Dec 2012 18:26:37 +0100 | blanchet | encode lemma name in file name | changeset | files |
Sat, 15 Dec 2012 21:07:52 +0100 | wenzelm | more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment; | changeset | files |
Sat, 15 Dec 2012 20:05:53 +0100 | wenzelm | prefer more official getMenuShortcutKeyMask, in deviation to traditional jEdit technique; | changeset | files |
Sat, 15 Dec 2012 18:30:09 +0100 | wenzelm | maintain subtree_elements for improved performance of cumulate operator; | changeset | files |
Sat, 15 Dec 2012 16:59:33 +0100 | wenzelm | more formal class Markup_Tree.Elements; | changeset | files |
Sat, 15 Dec 2012 14:45:08 +0100 | wenzelm | tuned command line; | changeset | files |
Sat, 15 Dec 2012 14:38:37 +0100 | wenzelm | merged | changeset | files |