src/Pure/Tools/jedit.ML
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;