apply small result immediately, to avoid visible delay of text update after window move;

structural equality for Command.Results; more general Command.State.eq_content;

allow fractional pretty margin -- avoid premature rounding;

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;