src/Pure/Syntax/parser.ML
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-03-01 wenzelm 2009-03-01 discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
2009-01-19 wenzelm 2009-01-19 removed Ids;
2008-11-18 wenzelm 2008-11-18 signed_string_of_int for priorities; tuned;
2008-08-09 wenzelm 2008-08-09 tuned error message;
2008-08-09 wenzelm 2008-08-09 datatype token: maintain range, tuned representation; tuned messages;
2008-04-16 haftmann 2008-04-16 educated guess for infix syntax
2008-02-14 wenzelm 2008-02-14 syntax error: suppress expected categories altogether;
2008-02-14 wenzelm 2008-02-14 expected syntax categories: reduced duplication, report minimal priorities only;
2008-01-26 wenzelm 2008-01-26 syntax error: unified output of priorities;
2008-01-26 wenzelm 2008-01-26 syntax error: reduced spam -- print expected nonterminals instead of terminals; tuned pretty_gram;
2007-08-13 wenzelm 2007-08-13 Lexicon.tokenize: do not appen EndToken yet;
2007-07-23 wenzelm 2007-07-23 avoid global reference warned'';
2007-07-22 wenzelm 2007-07-22 avoid polymorphic equality;
2007-04-03 wenzelm 2007-04-03 avoid clash with Alice keywords;
2006-11-28 wenzelm 2006-11-28 simplified '?' operator;
2006-10-10 haftmann 2006-10-10 gen_rem(s) abandoned in favour of remove / subtract
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality;
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-08 haftmann 2006-02-08 introduced gen_distinct in place of distinct
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-08 haftmann 2005-09-08 introduces some modern-style AList operations
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-31 haftmann 2005-08-31 introduced AList.*
2005-07-01 wenzelm 2005-07-01 avoid polyeq;
2005-05-17 wenzelm 2005-05-17 tuned;
2005-04-16 wenzelm 2005-04-16 added make_gram; merge_gram: do not add chain productions to prods;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-04-16 berghofe 2004-04-16 Replaced quote by Pretty.quote / Library.quote, since quote now refers to Symbol.quote
2002-03-14 kleing 2002-03-14 increased treshold for "this expression could be extremely ambigous" warning
2002-01-16 wenzelm 2002-01-16 GPLed;
1999-10-27 oheimb 1999-10-27 symbols in (error) messages now consistently with single backslash
1999-07-10 wenzelm 1999-07-10 more specific exn;
1999-06-25 wenzelm 1999-06-25 branching_level = 400;
1999-01-29 oheimb 1999-01-29 corrected output of symbols for several (probably not all) relevant functions
1998-05-12 wenzelm 1998-05-12 branching_level = 250;
1998-03-09 wenzelm 1998-03-09 tuned syntax error msg;
1997-12-28 wenzelm 1997-12-28 renamed Symtab.null to Symtab.empty;
1996-11-26 paulson 1996-11-26 Eta-expansion of a function definition, for value polymorphism
1996-11-14 wenzelm 1996-11-14 removed silly message;
1996-03-15 berghofe 1996-03-15 Added some functions which allow redirection of Isabelle's output
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-01-15 clasohm 1996-01-15 added comments
1995-07-03 clasohm 1995-07-03 removed debugging output
1995-07-03 clasohm 1995-07-03 added comments; fixed a bug; reduced memory usage slightly
1995-06-14 clasohm 1995-06-14 removed 'raw' productions from gram datatype; replaced mk_gram by add_prods; completely changed the generation of internal grammars to reuse existing ones in extend_gram
1995-02-02 clasohm 1995-02-02 simplified elimination of chain productions
1995-01-11 wenzelm 1995-01-11 pretty_gram: now sorts productions;
1994-12-08 clasohm 1994-12-08 changed Pure's grammar and the way types are converted to nonterminals
1994-11-09 clasohm 1994-11-09 changed warning for extremely ambiguous expressions
1994-11-03 clasohm 1994-11-03 added warning message "Currently parsed expression could be extremely ambiguous."
1994-10-04 clasohm 1994-10-04 made major changes to grammar; added call of Type.infer_types to automatically eliminate ambiguities
1994-08-19 wenzelm 1994-08-19 removed roots arg of extend_gram; added functor sig constraint (: PARSER);
1994-05-26 clasohm 1994-05-26 "Building new grammar" message is no longer displayed by empty_gram