Sat, 09 Aug 2008 00:09:35 +0200 datatype token: maintain range, tuned representation;
wenzelm [Sat, 09 Aug 2008 00:09:35 +0200] rev 27800
datatype token: maintain range, tuned representation; added eof, stopper (from simple_parse.ML); str_of_token: no special case for EOF; misc tuning;
Sat, 09 Aug 2008 00:09:34 +0200 tuned SymbolPos interface;
wenzelm [Sat, 09 Aug 2008 00:09:34 +0200] rev 27799
tuned SymbolPos interface;
Sat, 09 Aug 2008 00:09:31 +0200 YXML.parse: allow text without markup, potentially empty;
wenzelm [Sat, 09 Aug 2008 00:09:31 +0200] rev 27798
YXML.parse: allow text without markup, potentially empty;
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip