src/Pure/General/symbol.scala
2016-12-20 wenzelm 2016-12-20 tuned;
2016-11-10 wenzelm 2016-11-10 tuned comment;
2016-09-22 wenzelm 2016-09-22 discontinued raw symbols; discontinued Symbol.source; use initial Symbol.explode;
2016-07-20 wenzelm 2016-07-20 completion templates for commands involving "begin ... end" blocks;
2016-03-06 wenzelm 2016-03-06 clarified ML syntax for strings concerning UTF8;
2016-01-21 wenzelm 2016-01-21 tuned message;
2016-01-08 wenzelm 2016-01-08 clarified symbol insertion, depending on buffer encoding;
2016-01-08 wenzelm 2016-01-08 tuned;
2015-12-29 wenzelm 2015-12-29 tuned;
2015-12-19 wenzelm 2015-12-19 tuned signature;
2015-11-05 wenzelm 2015-11-05 symbolic syntax "\<comment> text";
2015-10-19 wenzelm 2015-10-19 added action "isabelle-emph"; changed shortcut of action "isabelle-reset";
2015-10-18 wenzelm 2015-10-18 clarified Symbol.is_control;
2015-10-09 wenzelm 2015-10-09 output HTML text according to Isabelle/Scala Symbol.Interpretation;
2015-09-14 wenzelm 2015-09-14 replacement character for spaces;
2015-05-03 wenzelm 2015-05-03 misc tuning, based on warnings by IntelliJ IDEA;
2014-12-08 wenzelm 2014-12-08 tuned signature;
2014-08-02 wenzelm 2014-08-02 tuned output;
2014-04-26 wenzelm 2014-04-26 tuned signature;
2014-04-08 wenzelm 2014-04-08 tuned;
2014-04-08 wenzelm 2014-04-08 more frugal Symbol.Index -- no need to waste space on mostly empty arrays;
2014-03-31 wenzelm 2014-03-31 proper structural hashCode, which is required for Command.File equals (NB: Array has physical object identity);
2014-03-31 wenzelm 2014-03-31 store blob content within document node: aux. files that were once open are made persistent; proper structural equality for Command.File and Symbol.Index;
2014-03-03 wenzelm 2014-03-03 tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
2014-02-20 wenzelm 2014-02-20 tuned imports;
2014-02-14 wenzelm 2014-02-14 lexical syntax for SML (in Scala); tuned;
2014-02-11 wenzelm 2014-02-11 tuned signature;
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-09-04 wenzelm 2013-09-04 expose basic Symbol.properties (uninterpreted);
2013-08-30 wenzelm 2013-08-30 sort items according to persistent history of frequency of use;
2013-08-30 wenzelm 2013-08-30 allow multiple symbol properties, notably groups and abbrevs;
2013-08-13 wenzelm 2013-08-13 discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end; document antiquotations: renamed term style "isub" to "sub";
2013-08-07 wenzelm 2013-08-07 tuned;
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;
2013-07-03 wenzelm 2013-07-03 tuned signature;
2012-12-16 wenzelm 2012-12-16 allow to suppress ISABELLE_SYMBOLS for experiments;
2012-11-30 wenzelm 2012-11-30 prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
2012-11-26 wenzelm 2012-11-26 more uniform Symbol.is_ascii_identifier in ML/Scala;
2012-11-26 wenzelm 2012-11-26 removed remains of Oheimb's double-space (cf. 0a5af667dc75);
2012-11-24 wenzelm 2012-11-24 tuned symbol groups;
2012-11-20 wenzelm 2012-11-20 support for symbol groups, retaining original order of declarations; updated WWW_Find: untested change of ad-hoc parser of ~~/etc/symbols;
2012-08-24 wenzelm 2012-08-24 more precise counting of line/column;
2012-08-11 wenzelm 2012-08-11 simplified symbol matching;
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-07-27 wenzelm 2012-07-27 tuned signature;
2012-07-17 wenzelm 2012-07-17 tuned imports;
2012-05-24 wenzelm 2012-05-24 less warning in scala-2.10.0-M3;
2012-03-26 wenzelm 2012-03-26 more precise treatment of \r\n as blank symbol (cf. 2bf29095d26f), e.g. relevant for loading theory headers in Isabelle/jEdit -- NB: jEdit and Isabelle/ML normalize newline variants to \n, but Isabelle/Scala retains them literally;
2012-03-17 wenzelm 2012-03-17 misc tuning to accomodate scala-2.10.0-M2;
2011-09-19 wenzelm 2011-09-19 refined Symbol.is_symbolic -- cover recoded versions as well;
2011-09-17 wenzelm 2011-09-17 Symbol.explode as in ML;
2011-08-17 wenzelm 2011-08-17 some convenience actions/shortcuts for control symbols;
2011-08-13 wenzelm 2011-08-13 tuned;
2011-07-09 wenzelm 2011-07-09 tuned signature;
2011-07-07 wenzelm 2011-07-07 explicit indication of type Symbol.Symbol;
2011-07-07 wenzelm 2011-07-07 simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style"; tuned implicit build/init messages;
2011-07-05 wenzelm 2011-07-05 simplified Symbol.iterator: produce strings, which are mostly preallocated; eliminated Symbol.CharSequence complications;