src/Pure/General/symbol.ML
Tue, 06 Jun 2017 13:13:25 +0200 wenzelm discontinued obsolete print mode;
Mon, 17 Oct 2016 15:46:51 +0200 wenzelm accomodate Poly/ML repository version, which treats singleton strings as boxed;
Thu, 22 Sep 2016 11:25:27 +0200 wenzelm discontinued raw symbols;
Tue, 05 Apr 2016 20:05:05 +0200 wenzelm avoid malformed Isabelle symbols during bootstrap;
Fri, 01 Apr 2016 18:56:31 +0200 wenzelm tuned signature;
Sun, 06 Mar 2016 16:19:02 +0100 wenzelm clarified treatment of fragments of Isabelle symbols during bootstrap;
Wed, 20 Jan 2016 14:32:56 +0100 wenzelm tuned signature (according to Scala version);
Sat, 19 Dec 2015 15:14:59 +0100 wenzelm tuned signature;
Thu, 19 Nov 2015 22:35:10 +0100 wenzelm tuned;
Thu, 05 Nov 2015 00:02:30 +0100 wenzelm symbolic syntax "\<comment> text";
Sun, 18 Oct 2015 20:48:24 +0200 wenzelm tuned signature;
Sun, 18 Oct 2015 17:20:20 +0200 wenzelm clarified Symbol.is_control;
Tue, 13 Oct 2015 21:27:30 +0200 wenzelm tuned signature (cf. XML.trim_blanks);
Sat, 01 Nov 2014 19:33:51 +0100 wenzelm recover via scanner;
Fri, 31 Oct 2014 22:02:49 +0100 wenzelm discontinued obsolete \<^sync> marker;
Sat, 18 Jan 2014 19:15:12 +0100 wenzelm support for nested text cartouches;
Fri, 13 Dec 2013 12:31:45 +0100 wenzelm clarified Proof General legacy: special treatment of \<^newline> only in TTY mode;
Thu, 12 Dec 2013 22:56:28 +0100 wenzelm discontinued legacy_isub_isup;
Wed, 04 Sep 2013 15:27:24 +0200 wenzelm some explicit indication of Proof General legacy;
Mon, 26 Aug 2013 10:33:16 +0200 wenzelm ignore trailing primes, e.g. rename \<alpha>' to \<alpha>'' instead of \<alpha>'a;
Tue, 13 Aug 2013 17:26:22 +0200 wenzelm disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
Thu, 08 Aug 2013 17:36:14 +0200 wenzelm more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;
Wed, 10 Jul 2013 16:25:26 +0200 wenzelm more robust identifier syntax: sub/superscript counts as modifier of LETDIG part instead of LETTER, both isub/isup and sub/sup are allowed;
Tue, 27 Nov 2012 19:22:36 +0100 wenzelm support for sub-structured identifier syntax (inactive);
Mon, 26 Nov 2012 21:46:04 +0100 wenzelm tuned signature;
Mon, 26 Nov 2012 21:10:42 +0100 wenzelm more uniform Symbol.is_ascii_identifier in ML/Scala;
Mon, 26 Nov 2012 20:58:41 +0100 wenzelm tuned;
Mon, 26 Nov 2012 20:39:19 +0100 wenzelm clarified Symbol.scan_ascii_id;
Mon, 26 Nov 2012 20:29:40 +0100 wenzelm tuned;
Mon, 26 Nov 2012 19:56:09 +0100 wenzelm removed remains of Oheimb's double-space (cf. 0a5af667dc75);
less more (0) -100 -50 -30 tip