Sat, 09 Aug 2008 00:09:39 +0200 read_token: more robust handling of empty text;
wenzelm [Sat, 09 Aug 2008 00:09:39 +0200] rev 27803
read_token: more robust handling of empty text;
Sat, 09 Aug 2008 00:09:38 +0200 datatype token: maintain range, tuned representation;
wenzelm [Sat, 09 Aug 2008 00:09:38 +0200] rev 27802
datatype token: maintain range, tuned representation; moved eof, stopper to lexicon.ML;
Sat, 09 Aug 2008 00:09:36 +0200 datatype token: maintain range, tuned representation;
wenzelm [Sat, 09 Aug 2008 00:09:36 +0200] rev 27801
datatype token: maintain range, tuned representation; tuned messages;
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;
Sat, 09 Aug 2008 00:09:29 +0200 added content;
wenzelm [Sat, 09 Aug 2008 00:09:29 +0200] rev 27797
added content; simplified implode: interface and permissive padding via Position.distance_of; added range; renamed implode_delim to implode_range;
Sat, 09 Aug 2008 00:09:26 +0200 added distance_of (permissive version);
wenzelm [Sat, 09 Aug 2008 00:09:26 +0200] rev 27796
added distance_of (permissive version); added no_range; tuned;
Fri, 08 Aug 2008 19:29:01 +0200 count offset as well;
wenzelm [Fri, 08 Aug 2008 19:29:01 +0200] rev 27795
count offset as well; more uniform treatment of invalid fields; tuned;
Fri, 08 Aug 2008 19:28:59 +0200 added offset/end_offset;
wenzelm [Fri, 08 Aug 2008 19:28:59 +0200] rev 27794
added offset/end_offset;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip