| 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 |