src/Tools/jEdit/etc/options
2016-06-22 ago report class parameters within instantiation;
2016-04-15 ago clarified rendering wrt. hyperlinks;
2016-04-15 ago tuned rendering;
2016-04-14 ago background color for entity def/ref focus;
2016-04-01 ago tuned;
2015-11-21 ago less intrusive rendering, notably for State dockable;
2015-10-15 ago report Markdown document structure;
2015-09-19 ago eliminated pointless jedit_text_overview_limit;
2015-09-08 ago disable jedit_auto_resolve (again) -- too confusing;
2015-08-25 ago clarified undefined_blobs: already loaded theories are suppressed;
2015-08-24 ago more explicit debugger caret rendering;
2015-08-19 ago disabled auto resolve, until practical consequences are more clear;
2015-08-12 ago resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
2015-08-12 ago tuned colors;
2015-08-12 ago clarified breakpoint rendering;
2015-08-10 ago tuned rendering;
2015-08-10 ago added action to toggle breakpoints (on editor side);
2015-08-10 ago rendering for debugger/breakpoint active state;
2015-03-19 ago tuned;
2015-01-05 ago GUI.imitate_font: more explicit result size, e.g. relevant for caching;
2014-12-30 ago explicit message channel for "legacy", which is nonetheless a variant of "warning";
2014-12-23 ago explicit message channels for "state", "information";
2014-12-10 ago more informative gutter content: fall-back on background color, e.g. when line numbers are enabled;
2014-12-09 ago proper alt_string markup (cf. 2ceb05ee0331);
2014-10-21 ago added option jedit_structure_limit;
2014-07-31 ago completion popup supports both ENTER and TAB (default);
2014-06-28 ago jedit_completion_immediate is enabled by default: let all users participate in slightly more ambitious symbol insertion;
2014-05-06 ago common support for search field, which is actually a light-weight Highlighter;
2014-05-06 ago tuned;
2014-05-03 ago support for path completion based on file-system content;
2014-05-03 ago yet another completion option, to imitate old less ambitious behavior;
2014-04-15 ago tuned default: melange of all "en" dialects;
2014-04-14 ago tuned;
2014-04-14 ago eliminated somewhat pointless locale parameter;
2014-04-13 ago added dictionaries_selector GUI;
2014-04-12 ago NEWS;
2014-04-12 ago more spell_checker_elements;
2014-04-12 ago more general spell_checker_elements;
2014-04-12 ago added spell-checker options;
2014-03-30 ago immediate completion even with delay, which is the default according to 638b29331549;
2014-03-18 ago more markup for improper elements;
2014-03-17 ago back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
2014-03-17 ago allow implicit semantic completion, notably after delay that exceeds usual round-trip time;
2014-03-12 ago clarified Markup.operator vs. Markup.delimiter;
2014-03-05 ago tuned color (cf. jEdit FUNCTION);
2014-03-05 ago more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
2014-02-27 ago simplified rendering -- no need to over-emphasize "token_range";
2014-02-25 ago more completion rendering: active, semantic, syntactic;
2014-02-24 ago tuned colors;
2014-02-24 ago clarified painting of invisible caret, e.g. focus change due to popup;
2014-02-17 ago more markup;
2014-02-15 ago more uniform ML keyword markup;
2014-01-18 ago support for nested text cartouches;
2013-12-30 ago added system option "jedit_print_mode";
2013-11-08 ago added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
2013-09-26 ago obsolete (see also 48d13465c7c7);
2013-09-25 ago bypass Isabelle OSX_Adapter for now -- MacOSX plugin 1.3 manages that better;
2013-09-18 ago added option "jedit_auto_load";
2013-09-14 ago tuned magic number, for improved reactivity on old 2-core machine;
2013-09-09 ago more robust Mac OS X application support;