src/Tools/jEdit/src/output2_dockable.scala
Tue, 18 Sep 2012 19:33:45 +0200 wenzelm pass base_snapshot to enable hyperlinks into other nodes;
Tue, 18 Sep 2012 17:20:40 +0200 wenzelm more explicit message markup and rendering;
Tue, 18 Sep 2012 13:36:28 +0200 wenzelm proper separation of output messages;
Tue, 18 Sep 2012 13:18:45 +0200 wenzelm some support for inital command markup;
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