| Fri, 14 Dec 2012 21:26:01 +0100 |
wenzelm |
init gutter according to view properties, which improves symmetry of windows and allows use of folds etc;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 12:09:08 +0100 |
wenzelm |
more formal class Command.Results;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 17:29:23 +0100 |
wenzelm |
more careful handling of Dialog_Result, with active area and color feedback;
|
file |
diff |
annotate
|
| Sat, 01 Dec 2012 19:51:43 +0100 |
wenzelm |
updated to jedit-5.0.0;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 16:22:29 +0100 |
wenzelm |
reset active areas on content update;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 20:59:32 +0100 |
wenzelm |
renamed main plugin object to PIDE;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 18:47:33 +0100 |
wenzelm |
quasi-abstract module Rendering, with Isabelle-specific implementation;
|
file |
diff |
annotate
|
| Sat, 24 Nov 2012 19:01:08 +0100 |
wenzelm |
prefer buffer_edit combinator over Java-style boilerplate;
|
file |
diff |
annotate
|
| Thu, 22 Nov 2012 17:01:20 +0100 |
wenzelm |
always refresh font metrics, to help window size calculation (amending 2585c81d840a);
|
file |
diff |
annotate
|
| Thu, 22 Nov 2012 15:22:27 +0100 |
wenzelm |
take component width as indication if it is already visible/layed-out, to avoid multiple formatting with minimal margin;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2012 21:08:20 +0100 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2012 18:28:31 +0200 |
wenzelm |
Rich_Text_Area tooltips via nested Pretty_Text_Area, based on some techniques of FoldViewer plugin;
|
file |
diff |
annotate
|
| Fri, 21 Sep 2012 21:24:33 +0200 |
wenzelm |
tighten margin for TextArea instead of Lobo;
|
file |
diff |
annotate
|
| Fri, 21 Sep 2012 15:39:51 +0200 |
wenzelm |
some support for hovering and sendback area;
|
file |
diff |
annotate
|
| Thu, 20 Sep 2012 22:25:30 +0200 |
wenzelm |
tuned painter;
|
file |
diff |
annotate
|
| Thu, 20 Sep 2012 20:27:47 +0200 |
wenzelm |
no caret painting;
|
file |
diff |
annotate
|
| Thu, 20 Sep 2012 20:13:42 +0200 |
wenzelm |
text_rendering as managed task, with cancellation;
|
file |
diff |
annotate
|
| Wed, 19 Sep 2012 17:27:37 +0200 |
wenzelm |
more direct GUI component;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 21:04:07 +0200 |
wenzelm |
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 19:50:09 +0200 |
wenzelm |
output is read-only;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 19:42:32 +0200 |
wenzelm |
token marker for extended syntax styles;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 19:33:45 +0200 |
wenzelm |
pass base_snapshot to enable hyperlinks into other nodes;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 14:51:12 +0200 |
wenzelm |
some actual rich text markup via XML.content_markup;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 13:18:45 +0200 |
wenzelm |
some support for inital command markup;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 11:49:23 +0200 |
wenzelm |
more static rendering state;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 11:43:05 +0200 |
wenzelm |
Pretty_Text_Area is based on Rich_Text_Area;
|
file |
diff |
annotate
|
| Sun, 16 Sep 2012 20:16:28 +0200 |
wenzelm |
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
|
file |
diff |
annotate
|