src/Pure/General/symbol.ML
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.
2004-06-22 wenzelm 2004-06-22 added chars_only, symbol_output;
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-20 wenzelm 2004-06-20 added escape, export encode_raw, default mode now trivial, tuned;
2004-06-17 wenzelm 2004-06-17 isub/isup quasi letter (again); tuned;
2004-06-16 wenzelm 2004-06-16 prevent looping of error messages involving malformed symbols;
2004-06-09 wenzelm 2004-06-09 tuned;
2004-06-05 wenzelm 2004-06-05 added datatype sym, val decode: symbol -> sym;
2004-05-29 wenzelm 2004-05-29 improved support for raw symbols;
2004-05-10 wenzelm 2004-05-10 tuned;
2004-04-26 wenzelm 2004-04-26 clarification of ascii vs. symbolic entities;
2004-04-19 kleing 2004-04-19 temporarily reverted quote change for release. breaks latex output, needs more testing.
2004-04-16 wenzelm 2004-04-16 tuned;
2004-04-16 berghofe 2004-04-16 Added variants of functions quote and commas_quote that allow escaping of " in error messages etc. This is useful for PGIP output.
2004-04-14 wenzelm 2004-04-14 proper handling of lines terminated by CRLF or CR;
2004-04-14 schirmer 2004-04-14 * raw control symbols are of the form \<^raw:...> now. * again allowing symbols to begin with "\\" instead of "\" for compatibility with ML-strings of old style theory and ML-files and isa-ProofGeneral.
2004-04-14 schirmer 2004-04-14 bugfix for \<^raw...> scanner
2004-04-13 schirmer 2004-04-13 * cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in the scanner * output functions default_output and xsymbols_output only print one "\" for symbols (to be consistent with the scanner).
2004-01-26 schirmer 2004-01-26 * Support for raw latex output in control symbols: \<^raw...> * Symbols may only start with one backslash: \<...>. \\<...> is no longer accepted by the scanner. - Adapted some Isar-theories to fit to this policy
2003-10-15 kleing 2003-10-15 use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid conflict with locale subscript syntax)
2003-10-15 kleing 2003-10-15 included \<^sub> in the range of identifier chars
2003-10-08 paulson 2003-10-08 now accepts DOS and Mac line breaks
2003-08-29 skalberg 2003-08-29 Removed the extended digits again.
2003-08-28 skalberg 2003-08-28 Extended the notion of letter and digit, such that now one may use greek, gothic, euler, or calligraphic letters as normal letters.
2002-11-27 berghofe 2002-11-27 default_output now escapes \'s more carefully.
2002-09-05 paulson 2002-09-05 added checking so that (rename_tac "x y") is rejected, since "x y" is not an identifier
2002-02-20 wenzelm 2002-02-20 added is_quasi; added bump_string (clarified version of old Library.bump_string);
2001-11-09 wenzelm 2001-11-09 got rid of obsolete input filtering;
2001-01-31 wenzelm 2001-01-31 added strip_blanks;
2001-01-21 wenzelm 2001-01-21 added spaces; added default_indent, indent;
2001-01-16 wenzelm 2001-01-16 export plain_output;
2000-12-29 wenzelm 2000-12-29 scan: malformed result;
2000-12-23 wenzelm 2000-12-23 tuned length;
2000-09-15 wenzelm 2000-09-15 updated;