src/Pure/General/symbol.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-16 wenzelm 2011-07-16 added File.fold_pages for streaming of large files; prefer \f notation;
2011-07-12 wenzelm 2011-07-12 tuned signature -- less cryptic ASCII names;
2011-06-20 wenzelm 2011-06-20 more tolerant Symbol.decode;
2011-06-17 wenzelm 2011-06-17 recovered markup for non-alphabetic keywords;
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-13 wenzelm 2010-11-13 simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.); allow malformed symbols inside quoted material, comments etc. -- for improved user experience with incremental re-parsing; refined treatment of malformed surrogates (Scala);
2010-11-12 wenzelm 2010-11-12 tuned signatures;
2010-10-25 wenzelm 2010-10-25 explicitly qualify type Output.output, which is a slightly odd internal feature;
2010-07-06 wenzelm 2010-07-06 implode pseudo utf8, i.e. decode byte-stuffed low ASCII characters;
2010-06-24 wenzelm 2010-06-24 escape UTF8 symbols for the ML compiler;
2010-06-24 wenzelm 2010-06-24 explicit treatment of UTF8 character sequences as Isabelle symbols;
2009-12-17 wenzelm 2009-12-17 robust representation of low ASCII control characters within XML/YXML text;
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-10 wenzelm 2009-11-10 removed obsolete name_of -- cf. decode;
2009-06-10 wenzelm 2009-06-10 discontinued escaped symbols such as \\<forall> -- only one backslash should be used;
2009-06-04 wenzelm 2009-06-04 export esc;
2009-04-28 haftmann 2009-04-28 Symbol.name_of and Name.desymbolize
2009-01-21 wenzelm 2009-01-21 removed Ids;
2009-01-02 wenzelm 2009-01-02 added output; improved encode_raw: map empty to empty; tuned;
2008-08-15 wenzelm 2008-08-15 scan: proper recovery for escaped \\< symbols;
2008-08-12 wenzelm 2008-08-12 Symbol.source/OuterLex.source: more explicit do_recover argument;
2008-08-07 wenzelm 2008-08-07 export not_eof;
2008-08-05 wenzelm 2008-08-05 improved recover: also resync on symbol/comment/verbatim delimiters;
2008-08-04 wenzelm 2008-08-04 abstract type Scan.stopper;
2008-04-12 wenzelm 2008-04-12 added is_utf8_trailer;
2008-04-03 wenzelm 2008-04-03 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
2008-04-03 wenzelm 2008-04-03 added some ASCII control symbols;
2007-12-15 wenzelm 2007-12-15 recover: not skip over "`";
2007-12-15 wenzelm 2007-12-15 added separate_chars;
2007-12-04 wenzelm 2007-12-04 symbol chi is also a letter;
2007-09-16 wenzelm 2007-09-16 added some int constraints (ML_Parse.fix_ints not active here);
2007-09-15 wenzelm 2007-09-15 replaced Symbol.is_hex_letter to Symbol.is_ascii_hex; tuned Symbol.is_ascii_blank (according to SML syntax);
2007-07-11 wenzelm 2007-07-11 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
2007-07-11 wenzelm 2007-07-11 Output.escape_malformed;
2007-07-10 wenzelm 2007-07-10 nested source: explicit interactive flag for recover avoids duplicate errors;
2007-07-09 wenzelm 2007-07-09 scan: changed treatment of malformed symbols, passed to next stage; tuned sym_explode;
2007-07-07 wenzelm 2007-07-07 simplified output mode setup; removed unused symbol_output; tuned;
2006-12-22 paulson 2006-12-22 fixed typo in comment
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-11-23 wenzelm 2006-11-23 removed obsolete alphanum;
2006-07-25 wenzelm 2006-07-25 raw symbols: disallow dot to avoid confusion in NameSpace.unpack;
2006-07-25 wenzelm 2006-07-25 added is/to_ascii_lower/upper; tuned alphanum -- needs more work;
2006-07-25 haftmann 2006-07-25 renamed Name.give_names to Name.names and moved Name.alphanum to Symbol.alphanum
2006-07-11 kleing 2006-07-11 hex and binary numerals (contributed by Rafal Kolanski)
2006-04-26 wenzelm 2006-04-26 tuned;
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality;
2006-03-14 wenzelm 2006-03-14 Output.add_mode: keyword component;
2006-02-06 wenzelm 2006-02-06 tuned;
2005-10-11 wenzelm 2005-10-11 raw symbols: allow non-ASCII chars (e.g. UTF-8); tuned comment;
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-09-01 wenzelm 2005-09-01 removed obsolete 'symbols' mode;
2005-08-16 wenzelm 2005-08-16 tuned Symbol.spaces;
2005-05-31 wenzelm 2005-05-31 added is_ident (from Syntax/lexicon.ML);
2005-05-18 wenzelm 2005-05-18 tuned;
2005-05-17 wenzelm 2005-05-17 tuned;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.