src/Tools/jEdit/src/jedit_options.scala
2014-07-23 wenzelm 2014-07-23 clarified module name: facilitate alternative GUI frameworks;
2014-04-26 wenzelm 2014-04-26 uniform focus traversal via TAB / Shift-TAB for all fields, in contrast to Java defaults, but in accordance to occasional jEdit practice;
2014-04-22 wenzelm 2014-04-22 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
2014-04-19 wenzelm 2014-04-19 clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
2014-04-17 wenzelm 2014-04-17 proper tooltip_lines for multi-line text;
2013-05-18 wenzelm 2013-05-18 explicit notion of public options, which are shown in the editor options dialog; avoid hard-wired stuff;
2013-04-04 wenzelm 2013-04-04 tuned signature -- concentrate GUI tools;
2012-10-04 wenzelm 2012-10-04 refined rich tooltip options; basic tooltips without markup;
2012-09-14 wenzelm 2012-09-14 more static handling of rendering options;
2012-09-12 wenzelm 2012-09-12 tuned error;
2012-09-11 wenzelm 2012-09-11 some GUI support for color options;
2012-09-11 wenzelm 2012-09-11 more informative tooltip: default value;
2012-09-11 wenzelm 2012-09-11 some support to organize options in sections;
2012-09-11 wenzelm 2012-09-11 prefer global default font over IsabelleText of jEdit TextArea;
2012-09-10 wenzelm 2012-09-10 proper multi-line tooltip;
2012-09-10 wenzelm 2012-09-10 more detailed option tooltip; more formal option.load; properties change propagation to Session_Dockable;
2012-09-10 wenzelm 2012-09-10 more systematic JEdit_Options.make_component; separate module Isabelle_Logic;
2012-09-10 wenzelm 2012-09-10 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);