src/Pure/Syntax/syntax.ML
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;
2007-01-19 wenzelm 2007-01-19 tuned Scan.extend_lexicon;
2006-12-30 wenzelm 2006-12-30 removed conditional combinator;
2006-12-13 wenzelm 2006-12-13 tuned signature;
2006-12-11 wenzelm 2006-12-11 advanced translation functions: Proof.context;
2006-12-09 wenzelm 2006-12-09 added internal_mode;
2006-12-07 wenzelm 2006-12-07 added input_mode;
2006-11-26 wenzelm 2006-11-26 extend_trtab: allow identical trfuns to be overwritten;
2006-09-29 wenzelm 2006-09-29 Syntax.mode;
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-05-02 wenzelm 2006-05-02 extend/remove_syntax: observe inout flag for translations, too;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-08 wenzelm 2006-04-08 pretty_term: late externing of consts (support authentic syntax);
2006-03-21 wenzelm 2006-03-21 subtract (op =);
2006-03-14 wenzelm 2006-03-14 added remove_trrules(_i); tuned;
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
2006-02-07 wenzelm 2006-02-07 renamed gen_duplicates to duplicates;
2006-02-06 wenzelm 2006-02-06 TableFun: renamed xxx_multi to xxx_list;
2006-02-03 wenzelm 2006-02-03 canonical member/insert/merge;
2006-01-31 wenzelm 2006-01-31 advanced translations: Context.generic;
2006-01-19 wenzelm 2006-01-19 added basic syntax; removed pure syntax;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2005-12-17 wenzelm 2005-12-17 sort_distinct;
2005-09-20 haftmann 2005-09-20 slight adaptions to library changes
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 wenzelm 2005-08-31 fixed ins_tokentr: AList.default;
2005-08-31 haftmann 2005-08-31 introduced AList.*
2005-08-28 wenzelm 2005-08-28 removed obsolete type_syn;
2005-08-16 wenzelm 2005-08-16 added eq_syntax;
2005-07-06 wenzelm 2005-07-06 tuned msg;
2005-07-01 wenzelm 2005-07-01 ambig msg: warning again;
2005-07-01 wenzelm 2005-07-01 use tracing for potentially voluminous ambiguity output;
2005-06-29 wenzelm 2005-06-29 proper treatment of advanced trfuns: pass thy argument; tuned warning;
2005-04-23 wenzelm 2005-04-23 removed token_trans.ML (some content moved to syn_ext.ML);
2005-04-17 wenzelm 2005-04-17 tuned;
2005-04-16 wenzelm 2005-04-16 expect translations functions to be stamped already; added remove_const_gram;
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
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-06-09 wenzelm 2004-06-09 removed separate logtypes field of syntax; removed test_read, simple_str_of_sort, simple_string_of_typ; provide default_mode;
2004-05-21 berghofe 2004-05-21 Modified functions pt_to_ast and ast_to_term to improve handling of errors in parse (ast) translations caused by ambiguous input.
2004-04-29 wenzelm 2004-04-29 added is_keyword;
2004-04-22 wenzelm 2004-04-22 tuned interfaces to accomodate advanced translation functions;
2004-04-16 berghofe 2004-04-16 Replaced quote by Library.quote, since quote now refers to Symbol.quote