Sat, 09 Aug 2008 12:28:11 +0200 pos_of_token: Position.T;
wenzelm [Sat, 09 Aug 2008 12:28:11 +0200] rev 27806
pos_of_token: Position.T; removed unused display_token; tuned;
Sat, 09 Aug 2008 12:28:10 +0200 dest: sort strings;
wenzelm [Sat, 09 Aug 2008 12:28:10 +0200] rev 27805
dest: sort strings; report: Output.status;
Sat, 09 Aug 2008 12:28:09 +0200 added literal;
wenzelm [Sat, 09 Aug 2008 12:28:09 +0200] rev 27804
added literal;
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;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip