src/Pure/Tools/jedit.ML
Tue, 10 Nov 2015 21:52:18 +0100 wenzelm tuned signature;
Tue, 10 Nov 2015 20:10:17 +0100 wenzelm clarified modules;
less more (0) tip