src/Pure/Syntax/syntax_ext.ML
Wed, 28 Dec 2016 10:39:50 +0100 wenzelm more uniform treatment of "bad" like other messages (with serial number);
Wed, 21 Sep 2016 22:43:06 +0200 wenzelm more general mixfix delimiters;
Mon, 05 Sep 2016 23:11:00 +0200 wenzelm clarified modules;
Fri, 01 Apr 2016 22:20:03 +0200 wenzelm explicit warning about formal use of Unicode;
Fri, 01 Apr 2016 21:34:17 +0200 wenzelm more markup;
Fri, 01 Apr 2016 19:01:34 +0200 wenzelm require actual space;
Fri, 01 Apr 2016 18:43:54 +0200 wenzelm tuned messages;
Fri, 01 Apr 2016 18:32:52 +0200 wenzelm clarified errors -- disallow cartouche fragments as delimiter;
Fri, 01 Apr 2016 17:14:27 +0200 wenzelm removed redundant Position.set_range -- already done in Position.range;
Fri, 01 Apr 2016 16:15:31 +0200 wenzelm explicit property for unbreakable block;
Fri, 01 Apr 2016 15:27:59 +0200 wenzelm tuned markup;
Fri, 01 Apr 2016 14:49:02 +0200 wenzelm clarified treatment of properties;
Thu, 31 Mar 2016 23:36:33 +0200 wenzelm explicit mixfix block properties;
Wed, 30 Mar 2016 22:35:41 +0200 wenzelm more language markup;
Wed, 30 Mar 2016 19:25:04 +0200 wenzelm more PIDE markup;
Wed, 30 Mar 2016 17:03:26 +0200 wenzelm clarified modules;
Wed, 30 Mar 2016 16:36:23 +0200 wenzelm clarified errors: more positions;
Tue, 29 Mar 2016 22:22:12 +0200 wenzelm tuned messages -- more positions;
Tue, 29 Mar 2016 21:17:29 +0200 wenzelm more position information for type mixfix;
Sun, 06 Mar 2016 16:19:02 +0100 wenzelm clarified treatment of fragments of Isabelle symbols during bootstrap;
Sun, 29 Mar 2015 19:24:07 +0200 wenzelm tuned signature;
Fri, 31 Oct 2014 22:02:49 +0100 wenzelm discontinued obsolete \<^sync> marker;
Sat, 25 May 2013 15:37:53 +0200 wenzelm syntax translations always depend on context;
Wed, 24 Aug 2011 23:00:53 +0200 wenzelm more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
Thu, 09 Jun 2011 20:22:22 +0200 wenzelm tuned signature: Name.invent and Name.invent_names;
Thu, 09 Jun 2011 15:38:49 +0200 wenzelm prefer new-style Name.invents;
Fri, 08 Apr 2011 22:40:29 +0200 wenzelm more accurate markup for syntax consts, notably binders which point back to the original logical entity;
Fri, 08 Apr 2011 21:11:29 +0200 wenzelm discontinued Syntax.max_pri, which is not really a symbolic parameter;
Fri, 08 Apr 2011 18:08:13 +0200 wenzelm simplified Pure syntax bootstrap;
Fri, 08 Apr 2011 17:45:37 +0200 wenzelm renamed sprop "prop#" to "prop'" -- proper identifier;
Fri, 08 Apr 2011 15:02:11 +0200 wenzelm discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
less more (0) tip