src/Tools/jEdit/src/pretty_text_area.scala
Thu, 22 Nov 2012 17:01:20 +0100 wenzelm always refresh font metrics, to help window size calculation (amending 2585c81d840a);
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;
Wed, 21 Nov 2012 21:08:20 +0100 wenzelm tuned comment;
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;
Fri, 21 Sep 2012 21:24:33 +0200 wenzelm tighten margin for TextArea instead of Lobo;
Fri, 21 Sep 2012 15:39:51 +0200 wenzelm some support for hovering and sendback area;
Thu, 20 Sep 2012 22:25:30 +0200 wenzelm tuned painter;
Thu, 20 Sep 2012 20:27:47 +0200 wenzelm no caret painting;
Thu, 20 Sep 2012 20:13:42 +0200 wenzelm text_rendering as managed task, with cancellation;
Wed, 19 Sep 2012 17:27:37 +0200 wenzelm more direct GUI component;
Tue, 18 Sep 2012 21:04:07 +0200 wenzelm minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
Tue, 18 Sep 2012 19:50:09 +0200 wenzelm output is read-only;
Tue, 18 Sep 2012 19:42:32 +0200 wenzelm token marker for extended syntax styles;
Tue, 18 Sep 2012 19:33:45 +0200 wenzelm pass base_snapshot to enable hyperlinks into other nodes;
Tue, 18 Sep 2012 14:51:12 +0200 wenzelm some actual rich text markup via XML.content_markup;
Tue, 18 Sep 2012 13:18:45 +0200 wenzelm some support for inital command markup;
Tue, 18 Sep 2012 11:49:23 +0200 wenzelm more static rendering state;
Tue, 18 Sep 2012 11:43:05 +0200 wenzelm Pretty_Text_Area is based on Rich_Text_Area;
Sun, 16 Sep 2012 20:16:28 +0200 wenzelm alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
less more (0) tip