src/Tools/jEdit/src/jedit/plugin.scala
2009-12-08 wenzelm 2009-12-08 misc modernization of names;
2009-12-08 wenzelm 2009-12-08 misc rearrangement of files;