src/Tools/jEdit/src/font_info.scala
2014-07-23 wenzelm 2014-07-23 clarified module name: facilitate alternative GUI frameworks;
2014-05-21 wenzelm 2014-05-21 more uniform Font_Info.Zoom_Box; misc tuning and clarification;
2014-04-22 wenzelm 2014-04-22 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
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;