wenzelm [Sat, 09 Aug 2008 22:43:46 +0200] rev 27809
unified Args.T with OuterLex.token, renamed some operations;
wenzelm [Sat, 09 Aug 2008 12:28:13 +0200] rev 27808
read_asts: report literal tokens;
wenzelm [Sat, 09 Aug 2008 12:28:12 +0200] rev 27807
tuned error message;
wenzelm [Sat, 09 Aug 2008 12:28:11 +0200] rev 27806
pos_of_token: Position.T;
removed unused display_token;
tuned;
wenzelm [Sat, 09 Aug 2008 12:28:10 +0200] rev 27805
dest: sort strings;
report: Output.status;
wenzelm [Sat, 09 Aug 2008 12:28:09 +0200] rev 27804
added literal;
wenzelm [Sat, 09 Aug 2008 00:09:39 +0200] rev 27803
read_token: more robust handling of empty text;
wenzelm [Sat, 09 Aug 2008 00:09:38 +0200] rev 27802
datatype token: maintain range, tuned representation;
moved eof, stopper to lexicon.ML;
wenzelm [Sat, 09 Aug 2008 00:09:36 +0200] rev 27801
datatype token: maintain range, tuned representation;
tuned messages;
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;