Sat, 23 Mar 2013 21:19:10 +0100 merged
wenzelm [Sat, 23 Mar 2013 21:19:10 +0100] rev 51499
merged
Sat, 23 Mar 2013 21:13:03 +0100 reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version;
wenzelm [Sat, 23 Mar 2013 21:13:03 +0100] rev 51498
reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version;
Sat, 23 Mar 2013 19:54:15 +0100 no censorship of "view.fracFontMetrics", although it often degrades rendering quality;
wenzelm [Sat, 23 Mar 2013 19:54:15 +0100] rev 51497
no censorship of "view.fracFontMetrics", although it often degrades rendering quality;
Sat, 23 Mar 2013 19:39:31 +0100 retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
wenzelm [Sat, 23 Mar 2013 19:39:31 +0100] rev 51496
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
Sat, 23 Mar 2013 16:46:09 +0100 apply small result immediately, to avoid visible delay of text update after window move;
wenzelm [Sat, 23 Mar 2013 16:46:09 +0100] rev 51495
apply small result immediately, to avoid visible delay of text update after window move;
Sat, 23 Mar 2013 16:10:46 +0100 structural equality for Command.Results;
wenzelm [Sat, 23 Mar 2013 16:10:46 +0100] rev 51494
structural equality for Command.Results; more general Command.State.eq_content;
Sat, 23 Mar 2013 13:57:46 +0100 allow fractional pretty margin -- avoid premature rounding;
wenzelm [Sat, 23 Mar 2013 13:57:46 +0100] rev 51493
allow fractional pretty margin -- avoid premature rounding;
Sat, 23 Mar 2013 13:12:39 +0100 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);
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;
Sat, 23 Mar 2013 13:04:28 +0100 tuned;
wenzelm [Sat, 23 Mar 2013 13:04:28 +0100] rev 51491
tuned;
Sat, 23 Mar 2013 20:57:57 +0100 spelling
haftmann [Sat, 23 Mar 2013 20:57:57 +0100] rev 51490
spelling
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip