| Tue, 18 Sep 2012 14:51:12 +0200 | wenzelm | some actual rich text markup via XML.content_markup; | changeset | files |
| Tue, 18 Sep 2012 13:36:28 +0200 | wenzelm | proper separation of output messages; | changeset | files |
| Tue, 18 Sep 2012 13:18:45 +0200 | wenzelm | some support for inital command markup; | changeset | files |
| Tue, 18 Sep 2012 11:49:23 +0200 | wenzelm | more static rendering state; | changeset | files |
| Tue, 18 Sep 2012 11:43:05 +0200 | wenzelm | Pretty_Text_Area is based on Rich_Text_Area; | changeset | files |
| Mon, 17 Sep 2012 20:34:19 +0200 | wenzelm | renamed Text_Area_Painter to Rich_Text_Area; | changeset | files |