Thu, 20 Sep 2012 21:57:37 +0200clarified message background;
wenzelm [Thu, 20 Sep 2012 21:57:37 +0200] rev 50489
clarified message background;

Thu, 20 Sep 2012 21:31:56 +0200tuned rendering;
wenzelm [Thu, 20 Sep 2012 21:31:56 +0200] rev 50488
tuned rendering;

Thu, 20 Sep 2012 20:27:47 +0200no caret painting;
wenzelm [Thu, 20 Sep 2012 20:27:47 +0200] rev 50487
no caret painting;

Thu, 20 Sep 2012 20:13:42 +0200text_rendering as managed task, with cancellation;
wenzelm [Thu, 20 Sep 2012 20:13:42 +0200] rev 50486
text_rendering as managed task, with cancellation;

Thu, 20 Sep 2012 19:23:05 +0200more management of Invoke_Scala tasks;
wenzelm [Thu, 20 Sep 2012 19:23:05 +0200] rev 50485
more management of Invoke_Scala tasks;

Thu, 20 Sep 2012 16:02:10 +0200more direct Markup_Tree.from_XML;
wenzelm [Thu, 20 Sep 2012 16:02:10 +0200] rev 50484
more direct Markup_Tree.from_XML;

Thu, 20 Sep 2012 15:00:14 +0200tuned signature;
wenzelm [Thu, 20 Sep 2012 15:00:14 +0200] rev 50483
tuned signature;

Thu, 20 Sep 2012 13:34:27 +0200more direct Markup_Tree.from_XML;
wenzelm [Thu, 20 Sep 2012 13:34:27 +0200] rev 50482
more direct Markup_Tree.from_XML;

Thu, 20 Sep 2012 11:09:53 +0200tuned signature;
wenzelm [Thu, 20 Sep 2012 11:09:53 +0200] rev 50481
tuned signature;

Thu, 20 Sep 2012 10:43:04 +0200tuned;
wenzelm [Thu, 20 Sep 2012 10:43:04 +0200] rev 50480
tuned;