| Sat, 23 Mar 2013 21:48:03 +0100 | wenzelm | prefer plain \<^sub> for better rendering (both in Isabelle/jEdit and LaTeX); | changeset | files |
| Sat, 23 Mar 2013 21:19:10 +0100 | wenzelm | merged | changeset | files |
| Sat, 23 Mar 2013 21:13:03 +0100 | wenzelm | reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version; | changeset | files |
| 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 |
| Sat, 23 Mar 2013 16:10:46 +0100 | wenzelm | structural equality for Command.Results; | changeset | files |