Thu, 17 Apr 2008 16:30:48 +0200 removed obsolete raw_str;
wenzelm [Thu, 17 Apr 2008 16:30:48 +0200] rev 26703
removed obsolete raw_str; added mark;
Thu, 17 Apr 2008 16:30:48 +0200 added markup for fixed variables (local constants);
wenzelm [Thu, 17 Apr 2008 16:30:48 +0200] rev 26702
added markup for fixed variables (local constants);
Thu, 17 Apr 2008 16:30:47 +0200 token translations: context dependent, result Pretty.T;
wenzelm [Thu, 17 Apr 2008 16:30:47 +0200] rev 26701
token translations: context dependent, result Pretty.T;
Thu, 17 Apr 2008 16:30:45 +0200 Pretty.mark;
wenzelm [Thu, 17 Apr 2008 16:30:45 +0200] rev 26700
Pretty.mark;
(0) -10000 -3000 -1000 -300 -100 -30 -10 -4 +4 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip