Sat, 23 Mar 2013 19:54:15 +0100 wenzelm no censorship of "view.fracFontMetrics", although it often degrades rendering quality;
Sat, 23 Mar 2013 19:39:31 +0100 wenzelm 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 wenzelm apply small result immediately, to avoid visible delay of text update after window move;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 tip