src/Tools/jEdit/etc/options
Tue, 18 Mar 2014 12:25:17 +0100 wenzelm more markup for improper elements;
Mon, 17 Mar 2014 23:16:26 +0100 wenzelm back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
Mon, 17 Mar 2014 10:45:29 +0100 wenzelm allow implicit semantic completion, notably after delay that exceeds usual round-trip time;
Wed, 12 Mar 2014 16:43:17 +0100 wenzelm clarified Markup.operator vs. Markup.delimiter;
Wed, 05 Mar 2014 19:57:41 +0100 wenzelm tuned color (cf. jEdit FUNCTION);
Wed, 05 Mar 2014 16:13:24 +0100 wenzelm more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
Thu, 27 Feb 2014 17:56:59 +0100 wenzelm simplified rendering -- no need to over-emphasize "token_range";
Tue, 25 Feb 2014 20:15:47 +0100 wenzelm more completion rendering: active, semantic, syntactic;
Mon, 24 Feb 2014 19:33:39 +0100 wenzelm tuned colors;
Mon, 24 Feb 2014 12:51:55 +0100 wenzelm clarified painting of invisible caret, e.g. focus change due to popup;
Mon, 17 Feb 2014 11:14:26 +0100 wenzelm more markup;
Sat, 15 Feb 2014 18:28:18 +0100 wenzelm more uniform ML keyword markup;
Sat, 18 Jan 2014 19:15:12 +0100 wenzelm support for nested text cartouches;
Mon, 30 Dec 2013 20:35:17 +0100 wenzelm added system option "jedit_print_mode";
Fri, 08 Nov 2013 17:34:37 +0100 wenzelm added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
Thu, 26 Sep 2013 13:28:26 +0200 wenzelm obsolete (see also 48d13465c7c7);
Wed, 25 Sep 2013 16:05:40 +0200 wenzelm bypass Isabelle OSX_Adapter for now -- MacOSX plugin 1.3 manages that better;
Wed, 18 Sep 2013 20:09:26 +0200 wenzelm added option "jedit_auto_load";
Sat, 14 Sep 2013 22:50:15 +0200 wenzelm tuned magic number, for improved reactivity on old 2-core machine;
Mon, 09 Sep 2013 16:15:48 +0200 wenzelm more robust Mac OS X application support;
Thu, 29 Aug 2013 21:53:29 +0200 wenzelm tuned;
Thu, 29 Aug 2013 21:17:46 +0200 wenzelm option to insert unique completion immediately into buffer;
Thu, 29 Aug 2013 10:24:43 +0200 wenzelm some completion options;
Tue, 27 Aug 2013 16:09:28 +0200 wenzelm determine completion geometry like tooltip;
Tue, 27 Aug 2013 15:35:51 +0200 wenzelm explicit "hidden" operation with focus management;
Fri, 23 Aug 2013 11:41:17 +0200 wenzelm added action isabelle.reset-font-size;
Mon, 05 Aug 2013 23:57:29 +0200 wenzelm query process animation;
Sat, 13 Jul 2013 18:13:09 +0200 wenzelm more rendering for information messages;
Sat, 13 Jul 2013 13:58:13 +0200 wenzelm gutter icon for information messages;
Sat, 13 Jul 2013 13:25:42 +0200 wenzelm more explicit Markup.information for messages produced by "auto" tools;
less more (0) -50 -30 tip