prefer plain \<^sub> for better rendering (both in Isabelle/jEdit and LaTeX); tuned proofs;

merged

reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version;

no censorship of "view.fracFontMetrics", although it often degrades rendering quality;

retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;

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;

tuned;