src/Pure/General/symbol_pos.ML
2011-07-23 wenzelm 2011-07-23 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
2011-07-12 wenzelm 2011-07-12 more precise Symbol_Pos.quote_string;
2011-07-08 wenzelm 2011-07-08 discontinued special treatment of hard tabulators;
2011-04-30 wenzelm 2011-04-30 more uniform variations of scan_string;
2010-12-29 wenzelm 2010-12-29 more scalable Symbol_Pos.explode;
2010-11-13 wenzelm 2010-11-13 eliminated slightly odd pervasive Symbol_Pos.symbol;
2010-05-17 wenzelm 2010-05-17 tuned signature;
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-03-19 wenzelm 2009-03-19 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML; scan_comment: recovered change_prompt; moved read_antiq to outer_lex.ML;
2009-03-18 wenzelm 2009-03-18 de-camelized Symbol_Pos;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-08-24 wenzelm 2008-08-24 untabify: silently turn tab into space if column information is unavailable;
2008-08-14 wenzelm 2008-08-14 made SML/NJ happy;
2008-08-13 wenzelm 2008-08-13 added untabify_content;
2008-08-09 wenzelm 2008-08-09 added content; simplified implode: interface and permissive padding via Position.distance_of; added range; renamed implode_delim to implode_range;
2008-08-07 wenzelm 2008-08-07 renamed SymbolPos.scan_position to SymbolPos.scan_pos; implode/explode: explicit type text = string; added implode_delim; explode: Position.reset_range;
2008-08-07 wenzelm 2008-08-07 Symbols with explicit position information.