On Sun, 11 Aug 2013, Thomas Bruederli wrote:
Increasing font size is a standard feature that every browser supports. Thus none of our default skins has such a functionality built in. But with the "extensible" skins it relatively easy to create a custom skin that supports this and still makes use of the templates and styles from the default skin.
I knocked together a small plugin which provides a drop down in the preferences offering three base font sizes:
Small : 11px (the standard setting from the Larry theme) Medium : 13px Large : 15px (the largest value which seems to be useful for me).
The plugin just pulls in an extra stylesheet of the form:
body { font-size: 13px; }
with extra fix ups to be added as required.
I still need to run some tests on different platforms to see what the knock on effects of messing with the font size are.
Half of hour of experimentation with the platforms available to me right now suggests that 13px works without ill effects, but that 15px really requires a large display to work. I do have to say that after comparing 11px, 13px and 15px, 11px does look very small.
My professors with poor eyesight also don't approve of the dark blue text on light blue background that Larry uses, but I can take much the same approach there. Presumably I will be able to move from local botch fixes using plugins to extensible skins at some point in the future?