src/Tools/jEdit/src/output_dockable.scala
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;
Sat, 14 Jan 2012 15:20:29 +0100 wenzelm tuned signature;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Wed, 07 Sep 2011 21:38:48 +0200 wenzelm clarified terminology;
Wed, 31 Aug 2011 17:22:49 +0200 wenzelm tuned Commands_Changed: cover nodes as well;
Tue, 30 Aug 2011 16:04:26 +0200 wenzelm tuned signature;
Mon, 04 Jul 2011 22:11:32 +0200 wenzelm quasi-static Isabelle_System -- reduced tendency towards "functorial style";
Thu, 23 Jun 2011 14:52:32 +0200 wenzelm explicit import java.lang.System to prevent odd scope problems;
Fri, 17 Jun 2011 13:55:53 +0200 wenzelm flush snapshot on falling edge of is_outdated -- recover effect of former buffer.propertiesChanged on text area (cf. f0770743b7ec);
Wed, 08 Jun 2011 17:42:07 +0200 wenzelm moved sources -- eliminated Netbeans artifact of jedit package directory;
less more (0) tip