src/Pure/Isar/parse.ML
Wed, 09 Apr 2014 17:54:09 +0200 wenzelm allow text cartouches in regular outer syntax categories "text" and "altstring";
Tue, 18 Mar 2014 12:25:17 +0100 wenzelm more markup for improper elements;
Tue, 18 Mar 2014 11:27:09 +0100 wenzelm tuned signature;
Wed, 12 Mar 2014 16:11:47 +0100 wenzelm more explicit markup for Token.Literal;
Sat, 01 Mar 2014 22:46:31 +0100 wenzelm clarified language markup: added "delimited" property;
Wed, 26 Feb 2014 11:14:38 +0100 wenzelm tuned;
Mon, 24 Feb 2014 10:17:29 +0100 wenzelm tuned signature;
Wed, 22 Jan 2014 16:03:11 +0100 wenzelm tuned signature;
Sat, 18 Jan 2014 19:15:12 +0100 wenzelm support for nested text cartouches;
Tue, 14 May 2013 19:48:31 +0200 wenzelm more uniform Markup.parse_real;
Tue, 09 Apr 2013 12:56:26 +0200 wenzelm just one syntax category "mixfix" -- check structure annotation semantically;
Fri, 05 Apr 2013 20:54:55 +0200 wenzelm tuned signature -- agree with markup terminology;
Sun, 26 Aug 2012 21:46:50 +0200 wenzelm theory def/ref position reports, which enable hyperlinks etc.;
Thu, 23 Aug 2012 17:46:03 +0200 wenzelm tuned messages: end-of-input rarely means physical end-of-file from the past;
Wed, 22 Aug 2012 12:47:49 +0200 wenzelm clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
Wed, 14 Mar 2012 17:52:38 +0100 wenzelm source positions for locale and class expressions;
Sun, 20 Nov 2011 16:58:12 +0100 wenzelm eliminated dead code;
Mon, 14 Nov 2011 16:52:19 +0100 wenzelm pass positions for named targets, for formal links in the document model;
Fri, 04 Nov 2011 00:07:45 +0100 wenzelm more liberal Parse.fixes, to avoid overlap of mixfix with is-pattern (notably in 'obtain' syntax);
Sun, 21 Aug 2011 20:42:26 +0200 wenzelm tuned Parse.group: delayed failure message;
Sat, 23 Jul 2011 16:37:17 +0200 wenzelm defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
Tue, 12 Jul 2011 15:12:50 +0200 wenzelm added Parse.properties (again) -- allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;
Tue, 03 May 2011 17:31:16 +0200 wenzelm more precise source position for @{rail};
Sun, 01 May 2011 18:05:09 +0200 wenzelm tuned;
Sat, 09 Apr 2011 23:29:50 +0200 wenzelm some position reports for 'translations';
Fri, 08 Apr 2011 22:59:52 +0200 wenzelm notation: proper markup for type constructor / constant;
Fri, 08 Apr 2011 22:50:50 +0200 wenzelm tuned signature;
Fri, 08 Apr 2011 21:11:29 +0200 wenzelm discontinued Syntax.max_pri, which is not really a symbolic parameter;
Fri, 08 Apr 2011 14:20:57 +0200 wenzelm discontinued special treatment of structure Mixfix;
Sun, 28 Nov 2010 21:07:28 +0100 wenzelm Parse.liberal_name for document antiquotations and attributes;
Sun, 28 Nov 2010 20:03:19 +0100 wenzelm added Parse.literal_fact with proper inner_syntax markup (source position);
Sun, 31 Oct 2010 13:26:37 +0100 wenzelm syntax category "real" subsumes plain "int";
Sat, 30 Oct 2010 15:26:40 +0200 wenzelm support for floating-point tokens in outer syntax (coinciding with inner syntax version);
Mon, 17 May 2010 15:11:25 +0200 wenzelm renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
Mon, 17 May 2010 10:20:55 +0200 wenzelm centralized legacy aliases;
Sat, 15 May 2010 22:24:25 +0200 wenzelm renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
less more (0) tip