src/Tools/jEdit/src/output_dockable.scala
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.;
Thu, 06 Dec 2012 22:12:25 +0100 wenzelm discontinued obsolete "Tracing" button -- limited tracing channel works sufficiently well;
Sun, 25 Nov 2012 21:23:20 +0100 wenzelm tuned signature;
Sun, 25 Nov 2012 21:10:29 +0100 wenzelm tuned signature;
Sun, 25 Nov 2012 20:59:32 +0100 wenzelm renamed main plugin object to PIDE;
Wed, 21 Nov 2012 14:06:59 +0100 wenzelm tuned;
Sun, 18 Nov 2012 15:28:58 +0100 wenzelm update options via protocol;
Wed, 17 Oct 2012 14:39:00 +0200 wenzelm added Output "Detach" button;
Thu, 11 Oct 2012 23:10:49 +0200 wenzelm refined separator: FBreak needs to be free for proper breaking, extra space at end helps to work around last-line oddity in jEdit;
Sun, 07 Oct 2012 16:05:31 +0200 wenzelm detach tooltip as dockable window;
Thu, 04 Oct 2012 19:31:50 +0200 wenzelm refined rich tooltip options;
Fri, 28 Sep 2012 16:51:58 +0200 wenzelm smarter handling of tracing messages;
Fri, 28 Sep 2012 15:45:03 +0200 wenzelm display number of tracing messages;
Sat, 22 Sep 2012 14:03:01 +0200 wenzelm tuned signature;
Fri, 21 Sep 2012 17:41:29 +0200 wenzelm merged
Fri, 21 Sep 2012 17:28:53 +0200 wenzelm renamed Output to Output1 and Output2 to Output, and thus make the new version the default;
Tue, 18 Sep 2012 17:20:40 +0200 wenzelm more explicit message markup and rendering;
Tue, 18 Sep 2012 13:18:45 +0200 wenzelm some support for inital command markup;
Mon, 17 Sep 2012 20:34:19 +0200 wenzelm renamed Text_Area_Painter to Rich_Text_Area;
Mon, 17 Sep 2012 20:23:25 +0200 wenzelm tuned signature -- more general Text_Area_Painter operations;
Fri, 14 Sep 2012 20:49:54 +0200 wenzelm refined output panel: more value-oriented approach to update and caret focus;
Tue, 11 Sep 2012 19:19:39 +0200 wenzelm more options;
Fri, 07 Sep 2012 13:58:54 +0200 wenzelm more explicit Delay operations;
Mon, 03 Sep 2012 10:17:17 +0200 wenzelm actually reset output when there is no valid command span here (especially relevant at very end of jEdit buffer, which lacks the terminating newline);
Tue, 29 May 2012 23:19:37 +0200 wenzelm update GUI components after init;
Thu, 19 Apr 2012 19:54:48 +0200 wenzelm more robust wrt. exceptions;
Wed, 18 Apr 2012 20:22:44 +0200 wenzelm more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
Mon, 19 Mar 2012 23:08:27 +0100 wenzelm explicit propagation of assignment event, even if changed command set is empty;
Thu, 01 Mar 2012 14:12:18 +0100 wenzelm explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
Tue, 21 Feb 2012 15:36:23 +0100 wenzelm overview.delay_repaint: avoid wasting GUI cycles via update_delay;
less more (0) -30 tip