src/Pure/General/symbol.ML
Sun, 28 Jan 2018 19:28:52 +0100 wenzelm clarified take/drop/chop prefix/suffix;
Sat, 27 Jan 2018 16:37:41 +0100 wenzelm more operations;
Sun, 14 Jan 2018 15:31:02 +0100 wenzelm clarified signature;
Sat, 13 Jan 2018 11:22:46 +0100 wenzelm added \<^cancel> operator for unused text;
Mon, 08 Jan 2018 14:26:45 +0100 wenzelm more operations;
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;
less more (0) -100 -50 -30 tip