src/Pure/Tools/jedit.ML
23 months ago wenzelm 2017-09-16 more derived actions, according to jEdit/org/gjt/sp/jedit/gui/DockableWindowFactory.java;
2016-08-12 wenzelm 2016-08-12 active jEdit actions;
2016-08-12 wenzelm 2016-08-12 more symbols;
2016-08-11 wenzelm 2016-08-11 clarified antiquotations;
2015-11-10 wenzelm 2015-11-10 more thorough check_action, including completion;
2015-11-10 wenzelm 2015-11-10 tuned signature;
2015-11-10 wenzelm 2015-11-10 clarified modules;