src/Pure/Syntax/lexicon.ML
Tue, 06 Sep 2011 20:37:07 +0200 wenzelm bulk reports for improved message throughput;
Sun, 04 Sep 2011 19:36:19 +0200 wenzelm eliminated markup for plain identifiers (frequent but insignificant);
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 ||);
Sat, 18 Jun 2011 12:37:42 +0200 wenzelm inner literal/delimiter corresponds to outer keyword/operator;
Tue, 26 Apr 2011 21:05:52 +0200 wenzelm clarified auxiliary structure Lexicon.Syntax;
Fri, 08 Apr 2011 16:34:14 +0200 wenzelm discontinued special treatment of structure Lexicon;
Wed, 06 Apr 2011 23:04:00 +0200 wenzelm separate structure Term_Position;
Tue, 22 Mar 2011 16:15:50 +0100 wenzelm update_name_tr: more precise handling of explicit constraints, including positions;
Tue, 22 Mar 2011 13:32:20 +0100 wenzelm support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
Mon, 21 Mar 2011 23:38:32 +0100 wenzelm added Lexicon.encode_position, Lexicon.decode_position;
Sat, 13 Nov 2010 19:47:23 +0100 wenzelm eliminated slightly odd pervasive Symbol_Pos.symbol;
Sat, 30 Oct 2010 15:26:40 +0200 wenzelm support for floating-point tokens in outer syntax (coinciding with inner syntax version);
Fri, 17 Sep 2010 21:04:56 +0200 wenzelm Syntax.read_asts error: report token ranges within message -- no side-effect here;
Fri, 17 Sep 2010 20:18:27 +0200 wenzelm tuned signature of (Context_)Position.report variants;
Tue, 07 Sep 2010 14:08:21 +0200 wenzelm report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
Wed, 18 Aug 2010 11:02:47 +0200 wenzelm uniform Markup.empty/Markup.Empty in ML and Scala;
Sun, 08 Aug 2010 19:54:54 +0200 wenzelm prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
Wed, 03 Mar 2010 00:00:44 +0100 wenzelm more systematic mark/unmark operations;
Sun, 21 Feb 2010 22:35:02 +0100 wenzelm slightly more abstract syntax mark/unmark operations;
Wed, 18 Mar 2009 21:55:38 +0100 wenzelm de-camelized Symbol_Pos;
Mon, 19 Jan 2009 20:05:41 +0100 wenzelm removed Ids;
Fri, 02 Jan 2009 19:38:13 +0100 wenzelm added numeral, which supercedes num, xnum, float;
Tue, 23 Dec 2008 19:27:42 +0100 wenzelm renamed terminal category "float" to "float_token", to avoid name
Sat, 29 Nov 2008 13:37:13 +0100 nipkow New lexical item "float".
Mon, 29 Sep 2008 21:26:41 +0200 wenzelm report_token/parse_token: back to context-less version;
Mon, 29 Sep 2008 14:41:25 +0200 wenzelm ContextPosition.report;
Fri, 15 Aug 2008 15:51:00 +0200 wenzelm token_kind: add Space, Comment;
Sat, 09 Aug 2008 12:28:11 +0200 wenzelm pos_of_token: Position.T;
Sat, 09 Aug 2008 00:09:35 +0200 wenzelm datatype token: maintain range, tuned representation;
Thu, 07 Aug 2008 13:45:13 +0200 wenzelm improved position handling due to SymbolPos.T;
less more (0) -50 -30 tip