Sat, 23 Mar 2013 19:54:15 +0100 | wenzelm | no censorship of "view.fracFontMetrics", although it often degrades rendering quality; | changeset | files |
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; | changeset | files |
Sat, 23 Mar 2013 16:46:09 +0100 | wenzelm | apply small result immediately, to avoid visible delay of text update after window move; | changeset | files |