wenzelm [Sat, 23 Mar 2013 13:12:39 +0100] rev 51492
more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
separate JEdit_Lib.pretty_metric, with slightly closer imitation of jEdit;