load args.ML later (after outer_parse.ML);

unified Args.T with OuterLex.token, renamed some operations;

read_asts: report literal tokens;

tuned error message;

pos_of_token: Position.T; removed unused display_token; tuned;

dest: sort strings; report: Output.status;

added literal;

read_token: more robust handling of empty text;

datatype token: maintain range, tuned representation; moved eof, stopper to lexicon.ML;

datatype token: maintain range, tuned representation; tuned messages;

datatype token: maintain range, tuned representation; added eof, stopper (from simple_parse.ML); str_of_token: no special case for EOF; misc tuning;

tuned SymbolPos interface;

YXML.parse: allow text without markup, potentially empty;

added content; simplified implode: interface and permissive padding via Position.distance_of; added range; renamed implode_delim to implode_range;

added distance_of (permissive version); added no_range; tuned;

count offset as well; more uniform treatment of invalid fields; tuned;

added offset/end_offset;

tuned formatting;

clean up dead code

made SML/NJ happy;

FundefLib.try_proof : attempt a proof and see if it works

added lemmas

inner_syntax markup is back;

disabled inner_syntax markup for now;

added read_token -- with optional YXML encoding of position; tuned parse operations: print position instead of echoing input (now encoded!); do not export obsolete read operation;

parse_token: use Syntax.read_token, pass full position information;

tuned;

map_default: more explicit scope;

datatype lexicon: alternative representation using nested Symtab.table;

simplified Antiquote signature;