src/Tools/jEdit/src/output_dockable.scala
Mon, 21 Sep 2015 11:45:03 +0200 wenzelm tuned;
Fri, 17 Jul 2015 21:45:15 +0200 wenzelm more uniform ComponentAdapter;
Wed, 23 Jul 2014 11:19:24 +0200 wenzelm clarified module name: facilitate alternative GUI frameworks;
Wed, 21 May 2014 16:21:11 +0200 wenzelm more uniform Font_Info.Zoom_Box;
Wed, 21 May 2014 14:42:45 +0200 wenzelm tuned signature;
Fri, 09 May 2014 21:03:44 +0200 wenzelm always bounce focus back to main text area, unless explicit focus component is given here (see also 7b65f4da136d);
Thu, 08 May 2014 21:14:25 +0200 wenzelm clarified detach_operation: ignore empty output;
Thu, 08 May 2014 21:03:05 +0200 wenzelm bounce focus back to main text area -- Output is for output, not query input;
Thu, 08 May 2014 11:47:38 +0200 wenzelm enable "PIDE" docking framework by default, and rely on its "Detach" menu item;
Thu, 08 May 2014 00:14:06 +0200 wenzelm some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
Tue, 06 May 2014 22:55:44 +0200 wenzelm tuned GUI layout;
Tue, 06 May 2014 21:29:17 +0200 wenzelm common support for search field, which is actually a light-weight Highlighter;
Tue, 06 May 2014 17:28:58 +0200 wenzelm more uniform detach button;
Tue, 06 May 2014 17:16:36 +0200 wenzelm tuned signature;
Fri, 25 Apr 2014 12:51:08 +0200 wenzelm clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
Tue, 22 Apr 2014 23:49:15 +0200 wenzelm avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
Thu, 27 Mar 2014 10:43:43 +0100 wenzelm more careful treatment of multiple command states (eval + prints): merge content that is actually required;
Sat, 01 Mar 2014 19:39:27 +0100 wenzelm tuned signature -- separate module Font_Info;
Thu, 20 Feb 2014 14:36:17 +0100 wenzelm tuned imports;
Tue, 24 Sep 2013 16:35:01 +0200 wenzelm skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
Wed, 18 Sep 2013 15:09:15 +0200 wenzelm improved FlowLayout for wrapping of components over multiple lines;
Sat, 24 Aug 2013 13:32:51 +0200 wenzelm more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
Mon, 12 Aug 2013 14:53:16 +0200 wenzelm prefer PIDE editor operations;
Mon, 12 Aug 2013 11:49:58 +0200 wenzelm tuned signature;
Fri, 02 Aug 2013 11:50:38 +0200 wenzelm tuned;
Thu, 04 Apr 2013 17:58:47 +0200 wenzelm tuned signature -- concentrate GUI tools;
Tue, 08 Jan 2013 16:25:22 +0100 wenzelm more aggressive update -- potentially relevant for previously is_outdated output;
Sat, 15 Dec 2012 12:01:07 +0100 wenzelm tuned signature;
Thu, 13 Dec 2012 17:29:23 +0100 wenzelm more careful handling of Dialog_Result, with active area and color feedback;
Thu, 13 Dec 2012 13:52:18 +0100 wenzelm identify dialogs via official serial and maintain as result message;
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) -60 tip