src/Tools/jEdit/src/font_info.scala
2014-03-01 wenzelm 2014-03-01 clarified module structure;
2014-03-01 wenzelm 2014-03-01 tuned;
2014-03-01 wenzelm 2014-03-01 tuned signature -- separate module Font_Info;