wenzelm [Wed, 16 Sep 2009 00:14:01 +0200] rev 34742
Linear_Set.append_after;
wenzelm [Tue, 15 Sep 2009 21:14:09 +0200] rev 34741
tuned file name;
wenzelm [Tue, 15 Sep 2009 20:46:46 +0200] rev 34740
tuned file name;
wenzelm [Tue, 15 Sep 2009 20:45:20 +0200] rev 34739
renamed PhaseOverviewPanel to Document_Overview;
wenzelm [Tue, 15 Sep 2009 20:39:00 +0200] rev 34738
tooltip: HTML dummy;
wenzelm [Tue, 15 Sep 2009 20:30:17 +0200] rev 34737
tuned;
wenzelm [Tue, 15 Sep 2009 19:50:10 +0200] rev 34736
misc tuning and unification;
wenzelm [Tue, 15 Sep 2009 19:01:16 +0200] rev 34735
refrain from actor shutdown -- slightly low-level;
wenzelm [Tue, 15 Sep 2009 18:14:28 +0200] rev 34734
keep BufferListener and TextAreaExtension private;
misc tuning;
wenzelm [Tue, 15 Sep 2009 18:13:30 +0200] rev 34733
tuned white space;