2012-09-14 wenzelm refined output panel: more value-oriented approach to update and caret focus;
2012-09-14 wenzelm clarified markup names;
2012-09-14 wenzelm more general Document_Model.point_range;
2012-09-14 wenzelm more static handling of rendering options;
2012-09-14 wenzelm tuned options (again);
2012-09-14 wenzelm more scalable option-group;
2012-09-14 nipkow tuned
Loading...
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip