src/Pure/Syntax/parser.ML
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
1994-05-19 clasohm 1994-05-19 lookaheads are now computed faster (during the grammar is built)
1994-05-17 clasohm 1994-05-17 fixed a bug in syntax_error, added "Building new grammar" message; automatically generated nonterminals now start with "@"
1994-05-13 clasohm 1994-05-13 syntax_error now checks precedences when computing expected tokens
1994-05-09 clasohm 1994-05-09 syntax_error now removes duplicate tokens in its output and doesn't print the last unparsed token (i.e. EndToken)
1994-05-06 clasohm 1994-05-06 improved syntax error: now shows correct number of unparsed tokens, a special message for unexpected EOF and a list of tokens that could continue the parsed input
1994-04-26 clasohm 1994-04-26 made a few cosmetic changes
1994-04-22 clasohm 1994-04-22 changed the way a grammar is generated to allow the new parser to work; also made a lot of changes in parser.ML and minor ones elsewhere
1994-02-03 wenzelm 1994-02-03 minor internal changes;
1994-01-19 wenzelm 1994-01-19 MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables now much leaner (eliminated gramgraph, all data except tables of old parser are shared); simplified the internal interfaces for syntax extension;
1993-10-08 wenzelm 1993-10-08 *** empty log message ***
1993-10-04 wenzelm 1993-10-04 lots of internal cleaning and tuning; removed {parse,print}_{pre,post}_proc; new lexer: now human readable due to scanner combinators; new parser installed, but still inactive (due to grammar ambiguities); added Syntax.test_read; typ_of_term: sorts now made distinct and sorted; mixfix: added forced line breaks (//); PROP now printed before subterm of type prop with non-const head;