src/Tools/jEdit/etc/options
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;
Wed, 10 Jul 2013 20:16:04 +0200 wenzelm less intrusive token_range rendering, which is relevant for inner parse errors;
Fri, 28 Jun 2013 14:51:19 +0200 wenzelm load icons via options -- prefer IntelliJ IDEA for now;
Tue, 21 May 2013 16:47:18 +0200 wenzelm less intrusive rendering of antiquoted text -- avoid visual clash with "blue variables" in particular;
Sat, 18 May 2013 12:41:31 +0200 wenzelm explicit notion of public options, which are shown in the editor options dialog;
Thu, 28 Mar 2013 22:42:18 +0100 wenzelm ghost bullet via markup, which is painted as bar under text (normally space);
Tue, 26 Mar 2013 11:26:13 +0100 wenzelm dockable window for timing information;
Mon, 18 Mar 2013 11:29:50 +0100 wenzelm extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
Sat, 16 Mar 2013 21:26:44 +0100 wenzelm more elementary tooltips via mouse events (imitating parts of javax.swing.ToolTipManager) -- avoid abuse of getToolTipText to produce window as side-effect;
Thu, 31 Jan 2013 22:21:05 +0100 wenzelm some native Mac OS X support, notably quit_handler (important for dialog on unsaved changes);
Sat, 15 Dec 2012 21:07:52 +0100 wenzelm more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
Wed, 12 Dec 2012 23:36:07 +0100 wenzelm rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
Wed, 12 Dec 2012 21:50:42 +0100 wenzelm support dialog via document content;
Mon, 10 Dec 2012 13:52:33 +0100 wenzelm generalized notion of active area, where sendback is just one application;
Thu, 06 Dec 2012 21:54:43 +0100 wenzelm discontinued option jedit_auto_start, which is somewhat pointless as there is no manual session start within Isabelle/jEdit;
Sat, 24 Nov 2012 17:12:06 +0100 wenzelm added option jedit_symbols_search_limit;
Mon, 22 Oct 2012 16:27:55 +0200 wenzelm further attempts to cope with large files via option jedit_text_overview_limit;
Fri, 05 Oct 2012 18:01:48 +0200 wenzelm eliminated obsolete tooltip delay -- bypassed by Pretty_Tooltip;
Fri, 05 Oct 2012 11:09:24 +0200 wenzelm tuned color and font size;
Thu, 04 Oct 2012 19:31:50 +0200 wenzelm refined rich tooltip options;
Thu, 04 Oct 2012 11:39:24 +0200 wenzelm option to bypass potentially slow text overview;
Fri, 21 Sep 2012 15:39:51 +0200 wenzelm some support for hovering and sendback area;
Thu, 20 Sep 2012 21:57:37 +0200 wenzelm clarified message background;
Thu, 20 Sep 2012 21:31:56 +0200 wenzelm tuned rendering;
Tue, 18 Sep 2012 17:20:40 +0200 wenzelm more explicit message markup and rendering;
Fri, 14 Sep 2012 18:12:41 +0200 wenzelm clarified markup names;
Fri, 14 Sep 2012 12:46:33 +0200 wenzelm tuned options (again);
Tue, 11 Sep 2012 23:26:03 +0200 wenzelm some GUI support for color options;
Tue, 11 Sep 2012 22:59:25 +0200 wenzelm more precise sections;
Tue, 11 Sep 2012 22:54:12 +0200 wenzelm provide color values via options;
Tue, 11 Sep 2012 19:19:39 +0200 wenzelm more options;
Tue, 11 Sep 2012 16:10:54 +0200 wenzelm replaced jedit_relative_font_size by jedit_font_scale;
Tue, 11 Sep 2012 15:47:42 +0200 wenzelm some support to organize options in sections;
Mon, 10 Sep 2012 21:17:32 +0200 wenzelm option jedit_load_delay;
Mon, 10 Sep 2012 15:20:50 +0200 wenzelm manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
less more (0) tip