| Wed, 21 Nov 2012 14:06:59 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 18 Nov 2012 15:28:58 +0100 |
wenzelm |
update options via protocol;
|
file |
diff |
annotate
|
| Wed, 17 Oct 2012 14:39:00 +0200 |
wenzelm |
added Output "Detach" button;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 07 Oct 2012 16:05:31 +0200 |
wenzelm |
detach tooltip as dockable window;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2012 19:31:50 +0200 |
wenzelm |
refined rich tooltip options;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 16:51:58 +0200 |
wenzelm |
smarter handling of tracing messages;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 15:45:03 +0200 |
wenzelm |
display number of tracing messages;
|
file |
diff |
annotate
|
| Sat, 22 Sep 2012 14:03:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 21 Sep 2012 17:41:29 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
| base
|
| Tue, 18 Sep 2012 17:20:40 +0200 |
wenzelm |
more explicit message markup and rendering;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 13:18:45 +0200 |
wenzelm |
some support for inital command markup;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 20:34:19 +0200 |
wenzelm |
renamed Text_Area_Painter to Rich_Text_Area;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 20:23:25 +0200 |
wenzelm |
tuned signature -- more general Text_Area_Painter operations;
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 20:49:54 +0200 |
wenzelm |
refined output panel: more value-oriented approach to update and caret focus;
|
file |
diff |
annotate
|
| Tue, 11 Sep 2012 19:19:39 +0200 |
wenzelm |
more options;
|
file |
diff |
annotate
|
| Fri, 07 Sep 2012 13:58:54 +0200 |
wenzelm |
more explicit Delay operations;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Tue, 29 May 2012 23:19:37 +0200 |
wenzelm |
update GUI components after init;
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 19:54:48 +0200 |
wenzelm |
more robust wrt. exceptions;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Mon, 19 Mar 2012 23:08:27 +0100 |
wenzelm |
explicit propagation of assignment event, even if changed command set is empty;
|
file |
diff |
annotate
|
| Thu, 01 Mar 2012 14:12:18 +0100 |
wenzelm |
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
|
file |
diff |
annotate
|
| Tue, 21 Feb 2012 15:36:23 +0100 |
wenzelm |
overview.delay_repaint: avoid wasting GUI cycles via update_delay;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 15:20:29 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 21:38:48 +0200 |
wenzelm |
clarified terminology;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2011 17:22:49 +0200 |
wenzelm |
tuned Commands_Changed: cover nodes as well;
|
file |
diff |
annotate
|
| Tue, 30 Aug 2011 16:04:26 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 04 Jul 2011 22:11:32 +0200 |
wenzelm |
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
|
file |
diff |
annotate
|
| Thu, 23 Jun 2011 14:52:32 +0200 |
wenzelm |
explicit import java.lang.System to prevent odd scope problems;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 17:42:07 +0200 |
wenzelm |
moved sources -- eliminated Netbeans artifact of jedit package directory;
|
file |
diff |
annotate
| base
|