src/Tools/jEdit/src/keymap_merge.scala
2016-09-01 wenzelm 2016-09-01 tuned message;
2016-09-01 wenzelm 2016-09-01 more robust persistent storage; tuned;
2016-09-01 wenzelm 2016-09-01 separate action; tuned message;
2016-09-01 wenzelm 2016-09-01 tuned message;
2016-09-01 wenzelm 2016-09-01 clarified GUI; tuned;
2016-09-01 wenzelm 2016-09-01 actual actions; tuned;
2016-09-01 wenzelm 2016-09-01 tuned;
2016-09-01 wenzelm 2016-09-01 clarified;
2016-09-01 wenzelm 2016-09-01 tuned GUI;
2016-08-31 wenzelm 2016-08-31 clarified GUI;
2016-08-31 wenzelm 2016-08-31 tuned GUI;
2016-08-31 wenzelm 2016-08-31 tuned rendering;
2016-08-31 wenzelm 2016-08-31 more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
2016-08-31 wenzelm 2016-08-31 clarified shortcut conflicts; tuned;
2016-08-30 wenzelm 2016-08-30 some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;