src/Pure/General/symbol.ML
2017-06-06 wenzelm 2017-06-06 discontinued obsolete print mode;
2016-10-17 wenzelm 2016-10-17 accomodate Poly/ML repository version, which treats singleton strings as boxed;
2016-09-22 wenzelm 2016-09-22 discontinued raw symbols; discontinued Symbol.source; use initial Symbol.explode;
2016-04-05 wenzelm 2016-04-05 avoid malformed Isabelle symbols during bootstrap;
2016-04-01 wenzelm 2016-04-01 tuned signature;
2016-03-06 wenzelm 2016-03-06 clarified treatment of fragments of Isabelle symbols during bootstrap;
2016-01-20 wenzelm 2016-01-20 tuned signature (according to Scala version);
2015-12-19 wenzelm 2015-12-19 tuned signature;
2015-11-19 wenzelm 2015-11-19 tuned;
2015-11-05 wenzelm 2015-11-05 symbolic syntax "\<comment> text";
2015-10-18 wenzelm 2015-10-18 tuned signature;
2015-10-18 wenzelm 2015-10-18 clarified Symbol.is_control;
2015-10-13 wenzelm 2015-10-13 tuned signature (cf. XML.trim_blanks);
2014-11-01 wenzelm 2014-11-01 recover via scanner; tuned signature;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete \<^sync> marker;
2014-01-18 wenzelm 2014-01-18 support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;
2013-12-13 wenzelm 2013-12-13 clarified Proof General legacy: special treatment of \<^newline> only in TTY mode;
2013-12-12 wenzelm 2013-12-12 discontinued legacy_isub_isup;
2013-09-04 wenzelm 2013-09-04 some explicit indication of Proof General legacy;
2013-08-26 wenzelm 2013-08-26 ignore trailing primes, e.g. rename \<alpha>' to \<alpha>'' instead of \<alpha>'a;
2013-08-13 wenzelm 2013-08-13 disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
2013-08-08 wenzelm 2013-08-08 more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;
2013-07-10 wenzelm 2013-07-10 more robust identifier syntax: sub/superscript counts as modifier of LETDIG part instead of LETTER, both isub/isup and sub/sup are allowed;
2012-11-27 wenzelm 2012-11-27 support for sub-structured identifier syntax (inactive);
2012-11-26 wenzelm 2012-11-26 tuned signature; tuned;
2012-11-26 wenzelm 2012-11-26 more uniform Symbol.is_ascii_identifier in ML/Scala;
2012-11-26 wenzelm 2012-11-26 tuned;
2012-11-26 wenzelm 2012-11-26 clarified Symbol.scan_ascii_id; ATP: follow change from Symbol.scan_id to Symbol.scan_ascii_id, assuming that this was meant here, not fully symbolic Isabelle identifiers;
2012-11-26 wenzelm 2012-11-26 tuned;
2012-11-26 wenzelm 2012-11-26 removed remains of Oheimb's double-space (cf. 0a5af667dc75);
2012-11-22 wenzelm 2012-11-22 some support for breakable text and paragraphs; tuned Symbol.scanner, which operates on symbols, not characters;
2012-08-11 wenzelm 2012-08-11 further clarification of malformed symbols;
2012-08-11 wenzelm 2012-08-11 more liberal scanning of potentially malformed symbols;
2012-08-07 wenzelm 2012-08-07 tuned signature -- make Pretty less dependent on Symbol;
2012-05-02 wenzelm 2012-05-02 avoid interference of markup for literal tokens, which may contain slightly odd \<^bsub> \<^esub> counted as pseudo-markup (especially relevant for HTML output, e.g. of thm power3_eq_cube);
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;