src/Tools/jEdit/etc/options
2012-10-05 wenzelm tuned color and font size;
2012-10-04 wenzelm refined rich tooltip options;
2012-10-04 wenzelm option to bypass potentially slow text overview;
2012-09-21 wenzelm some support for hovering and sendback area;
2012-09-20 wenzelm clarified message background;
2012-09-20 wenzelm tuned rendering;
2012-09-18 wenzelm more explicit message markup and rendering;
2012-09-14 wenzelm clarified markup names;
2012-09-14 wenzelm tuned options (again);
2012-09-11 wenzelm some GUI support for color options;
2012-09-11 wenzelm more precise sections;
2012-09-11 wenzelm provide color values via options;
2012-09-11 wenzelm more options;
2012-09-11 wenzelm replaced jedit_relative_font_size by jedit_font_scale;
2012-09-11 wenzelm some support to organize options in sections;
2012-09-10 wenzelm option jedit_load_delay;
2012-09-10 wenzelm manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
less more (0) tip