src/Pure/Syntax/syn_ext.ML
2004-06-09 wenzelm 2004-06-09 removed separate logtypes field of syntax;
2004-05-29 wenzelm 2004-05-29 Library.read_int;
2004-05-01 wenzelm 2004-05-01 improved indexed syntax / implicit structures;
2004-04-22 wenzelm 2004-04-22 non_typed_tr';
2002-01-30 wenzelm 2002-01-30 escape_mfix;
2002-01-16 wenzelm 2002-01-16 GPLed;
2001-12-14 wenzelm 2001-12-14 support for ``indexed syntax'' (using "\<index>" argument instead of "_");
2001-09-01 wenzelm 2001-09-01 tuned;
2000-07-17 wenzelm 2000-07-17 consts: include *all* names;
1999-09-04 wenzelm 1999-09-04 removed binding;
1999-06-02 wenzelm 1999-06-02 added dddot_indexname;
1999-03-09 wenzelm 1999-03-09 token translation: real;
1998-11-16 wenzelm 1998-11-16 Scan.read;
1998-10-20 wenzelm 1998-10-20 no open;
1998-05-18 wenzelm 1998-05-18 Symbol.stopper;
1998-03-09 wenzelm 1998-03-09 adapted to new scanner and abroque chars;
1997-11-05 wenzelm 1997-11-05 adapted syn_ext_trfunsT;
1997-10-31 wenzelm 1997-10-31 tuned;
1997-10-30 wenzelm 1997-10-30 added mixfix_args;
1997-04-04 wenzelm 1997-04-04 fixed diagnostic output of print modes;
1997-02-28 wenzelm 1997-02-28 added token_translation interface;
1996-12-13 wenzelm 1996-12-13 added fix_tr', syn_ext_trfunsT; changed syn_ext_trfuns (fix_tr');
1996-12-10 wenzelm 1996-12-10 mfix_to_xprod: now uses read_charnames;
1996-11-27 wenzelm 1996-11-27 changed symbolic char syntax to \<NAME>
1996-11-19 wenzelm 1996-11-19 minor tuning;
1996-11-18 wenzelm 1996-11-18 new delimiter syntax in mixfixes: \{SYMBOLNAME} is char from symbol font;
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.
1995-07-03 clasohm 1995-07-03 added cargs for curried function application
1995-06-12 clasohm 1995-06-12 fixed bug in mfix_to_xprod: lambda productions' lhs shouldn't be modified
1995-03-03 clasohm 1995-03-03 added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1995-02-27 wenzelm 1995-02-27 new in mixfix annotations: "' " (quote space) separates delimiters without adding extra white space for printing;
1995-01-18 clasohm 1995-01-18 added optional precedence for body of binder; removed call to infer_types from read_xrules
1994-12-14 wenzelm 1994-12-14 removed "logic1"; improved typ_to_nonterm;
1994-12-08 clasohm 1994-12-08 changed Pure's grammar and the way types are converted to nonterminals
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 idT, varT, tidT, tvarT (now in lexicon.ML); added syn_ext_const_names, syn_ext_trfuns;
1994-06-29 clasohm 1994-06-29 changed precedence of constrain to [4, 0], 3
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-11 clasohm 1994-05-11 changed implode to ^
1994-05-11 clasohm 1994-05-11 moved 'filter is_xid' in syn_ext
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-01-19 wenzelm 1994-01-19 contains remaining parts of xgram.ML and extension.ML; syn_ext replaces xgram and ext;