On Tue, 25 Aug 2015, Rafal Kolanski wrote:
- Removes hardcoded colors in favor of looking up relevant JEdit
properties. This is critical if you want a light-on-dark setup.
Also in patches/extended_styles style[0] is hardcoded to black
in org/gjt/sp/util/SyntaxUtilities.java. This should really look
up the view.fgColor property in JEdit!
Generally, defaulting to BLACK for foreground is inflexible, use:
jEdit.getColorProperty("view.fgColor")
same for 255,255,255 for a background, try use:
jEdit.getColorProperty("view.bgColor")
I wonder where this strange light-on-dark trend is coming from, maybe from
mobile devices? Many decades ago, monitor display quality was too poor
for proper black-on-white text, which is why I consider this as luxory.
Anyway, hardwired values are bad. I've changed most of them in
1d9c121cbe4d and 9791f631c20d.
The patched jedit code base will be updated again for the coming release
of 5.3.0, which should appear *really*soon*now*. It will be the first
jEdit release with proper 4K display support!
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
