| Fri, 14 Sep 2012 20:49:54 +0200 | wenzelm | refined output panel: more value-oriented approach to update and caret focus; | changeset | files |
| Fri, 14 Sep 2012 18:12:41 +0200 | wenzelm | clarified markup names; | changeset | files |
| Fri, 14 Sep 2012 17:37:19 +0200 | wenzelm | more general Document_Model.point_range; | changeset | files |
| Fri, 14 Sep 2012 13:52:16 +0200 | wenzelm | more static handling of rendering options; | changeset | files |
| Fri, 14 Sep 2012 12:46:33 +0200 | wenzelm | tuned options (again); | changeset | files |
| Fri, 14 Sep 2012 12:29:02 +0200 | wenzelm | more scalable option-group; | changeset | files |
| Fri, 14 Sep 2012 10:01:42 +0200 | nipkow | tuned | changeset | files |