src/Pure/Syntax/syntax.ML
2010-02-27 wenzelm 2010-02-27 parallel brute-force disambiguation;
2010-02-21 wenzelm 2010-02-21 filter out authentic const syntax;
2010-02-15 wenzelm 2010-02-15 renamed InfixName to Infix etc.;
2010-02-11 wenzelm 2010-02-11 added ML antiquotation @{syntax_const};
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-29 wenzelm 2009-11-29 tuned message;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-03-18 wenzelm 2009-03-18 de-camelized Symbol_Pos;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-01 wenzelm 2009-03-01 discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
2008-12-17 haftmann 2008-12-17 dropped Ids
2008-12-05 haftmann 2008-12-05 removed Table.extend, NameSpace.extend_table
2008-11-29 nipkow 2008-11-29 New lexical item "float".
2008-11-18 wenzelm 2008-11-18 tuned;
2008-09-29 wenzelm 2008-09-29 report_token/parse_token: back to context-less version;
2008-09-29 wenzelm 2008-09-29 ContextPosition.report; parse_token/report_token: explicit context;
2008-09-26 wenzelm 2008-09-26 eliminated polymorphic equality;
2008-08-15 wenzelm 2008-08-15 read_asts: Lexicon.report_token, filter Lexicon.is_proper; report tokens;
2008-08-10 wenzelm 2008-08-10 added parse_token (from proof_context.ML);
2008-08-09 wenzelm 2008-08-09 read_asts: report literal tokens;
2008-08-09 wenzelm 2008-08-09 read_token: more robust handling of empty text;
2008-08-07 wenzelm 2008-08-07 added read_token -- with optional YXML encoding of position; tuned parse operations: print position instead of echoing input (now encoded!); do not export obsolete read operation;
2008-08-07 wenzelm 2008-08-07 adapted Scan.extend_lexicon/merge_lexicons;
2008-06-18 wenzelm 2008-06-18 TypeExt.type_constraint;
2008-06-13 wenzelm 2008-06-13 map_const: soft version, no failure here;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax; reordered signature;
2008-04-17 wenzelm 2008-04-17 token translations: context dependent, result Pretty.T; string_of_term/prop: Variable.auto_fixes;
2008-04-16 wenzelm 2008-04-16 tuned;
2008-04-16 haftmann 2008-04-16 educated guess for infix syntax
2008-01-27 wenzelm 2008-01-27 added ambiguity_limit (restricts parse trees / terms printed in messages); tuned;
2007-11-27 wenzelm 2007-11-27 standard_parse_term: check ambiguous results without changing the result yet;
2007-11-11 wenzelm 2007-11-11 syntax operations: turned extend'' into update'' (absorb duplicates); tuned signature;
2007-11-10 wenzelm 2007-11-10 added update_const_gram (avoids duplicates); tuned;
2007-10-20 wenzelm 2007-10-20 moved internalM to PrintMode.internal; PrintMode.input;
2007-10-16 wenzelm 2007-10-16 Syntax.(un)check: explicit result option;
2007-10-15 wenzelm 2007-10-15 unparse_arity: unparse type constructor as well;
2007-10-11 wenzelm 2007-10-11 renamed Syntax.XXX_mode to Syntax.mode_XXX; moved ProofContext.pp to Syntax.pp;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations; added uncheck/unparse_classrel/arity (from sign.ML); tuned;
2007-09-29 wenzelm 2007-09-29 added unparse interfaces (still unused); add_typ/term_check: added stage and name argument; added print_checks;
2007-09-25 wenzelm 2007-09-25 removed redundant global_parse operations; renamed global_XXX to XXX_global;
2007-09-23 wenzelm 2007-09-23 TypeInfer.constrain: canonical argument order;
2007-09-17 wenzelm 2007-09-17 added print_mode_value (CRITICAL);
2007-09-01 wenzelm 2007-09-01 added singleton check_typ/term/prop;
2007-08-30 wenzelm 2007-08-30 turned type_check into separate typ/term_check; tuned sifnature;
2007-08-20 wenzelm 2007-08-20 standard_parse_term: added pp/check argument, include disambig here (from sign.ML);
2007-08-20 wenzelm 2007-08-20 type_check: tuned singleton funs case;
2007-08-14 wenzelm 2007-08-14 renamed standard_read_XXX to standard_parse_XXX; added global_read/parse_XXX;
2007-08-14 wenzelm 2007-08-14 added generic wrapper for parse/read functions; renamed read_term to standard_read_term etc.;
2007-08-13 wenzelm 2007-08-13 moved appl syntax to PureThy; structure Lexicon: not hidden;
2007-07-23 wenzelm 2007-07-23 hide internal structures (again);
2007-07-09 wenzelm 2007-07-09 type output = string indicates raw system output;
2007-07-08 wenzelm 2007-07-08 replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-07-07 wenzelm 2007-07-07 pretty_sort/typ/term: markup;
2007-07-07 wenzelm 2007-07-07 simplified pretty token metric: type int;
2007-04-21 wenzelm 2007-04-21 TypeExt.decode_term;
2007-04-15 wenzelm 2007-04-15 added read_term; adapted decoding of types/sorts;
2007-04-03 wenzelm 2007-04-03 avoid clash with Alice keywords;