src/Pure/Syntax/type_ext.ML
2011-04-03 wenzelm 2011-04-03 added Position.reports convenience; modernized Syntax.trrule constructors; modernized Sign.add_trrules/del_trrules: internal arguments; modernized Isar_Cmd.translations/no_translations: external arguments; explicit syntax categories class_name/type_name, with reports via type_context; eliminated former class_name/type_name ast translations; tuned signatures;
2011-03-30 wenzelm 2011-03-30 more informative markup_free;
2011-03-27 wenzelm 2011-03-27 decode_term: some context-sensitive markup; more informative Markup.entity and Name_Space.markup_entry; Markup.const: use "constant" to make it coincide with name space kind;
2011-03-27 wenzelm 2011-03-27 tuned signatures;
2011-03-27 wenzelm 2011-03-27 decode_term: more precise reports;
2011-03-27 wenzelm 2011-03-27 decode_term/disambig: report resolved term variables for the unique (!) result;
2011-03-22 wenzelm 2011-03-22 update_name_tr: more precise handling of explicit constraints, including positions;
2011-03-22 wenzelm 2011-03-22 statespace syntax: strip positions -- type constraints are unexpected here;
2011-03-22 wenzelm 2011-03-22 datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
2011-03-22 wenzelm 2011-03-22 support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive; simplified/generalized abs_tr/binder_tr: allow iterated constraints, stemming from positions; Ast.pretty_ast: special treatment of encoded positions; eliminated Ast.str_of_ast in favour of uniform Ast.pretty_ast;
2010-09-12 wenzelm 2010-09-12 eliminated aliases of Type.constraint;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-04-29 wenzelm 2010-04-29 uniform decoding of fixed/const syntax entities, allows to pass "\<^fixed>foo__" through the syntax layer (supersedes 1b7109c10b7b);
2010-04-28 wenzelm 2010-04-28 get_sort: minimize sorts given in the text, while keeping those from the context unchanged (the latter are preferred); tuned;
2010-03-09 wenzelm 2010-03-09 simplified Syntax.basic_syntax (again); separate Syntax.type_ast_trs depending on read_class/read_type;
2010-03-03 wenzelm 2010-03-03 "_type_prop" is syntax const -- recovered printing of OFCLASS;
2010-03-03 wenzelm 2010-03-03 authentic syntax for classes and type constructors; read/intern formal entities just after raw parsing, extern just before final pretty printing; discontinued _class token translation; moved Local_Syntax.extern_term to Syntax/printer.ML; misc tuning;
2010-02-21 wenzelm 2010-02-21 slightly more abstract syntax mark/unmark operations;
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-01-19 wenzelm 2009-01-19 removed Ids;
2008-06-18 wenzelm 2008-06-18 added type_constraint (formerly in type_infer.ML, which is now loaded later);
2008-06-13 wenzelm 2008-06-13 map_const: soft version, no failure here (recovers hiding of consts, because a hidden name is illegal and rejected later);
2008-04-17 wenzelm 2008-04-17 moved default token translations to proof_context.ML, if all fails the pretty printer falls back on plain output;
2008-02-04 wenzelm 2008-02-04 *** MESSAGE REFERS TO 1.29 and 1.44 *** sort_of_term: be permissive about _class *output* markers, to allow print translations invoke this function as well;
2008-02-01 haftmann 2008-02-01 fixed term_of_sort
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-05-31 wenzelm 2007-05-31 decode_term: force qualified name into Const;
2007-04-21 wenzelm 2007-04-21 TypeExt.decode_term;
2007-04-15 wenzelm 2007-04-15 added decode_types (from type_infer.ML); decode sorts: internalize here; tuned;
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality;
2005-06-29 wenzelm 2005-06-29 export no_type_brackets; accomodate advanced trfuns; tuned;
2005-04-23 wenzelm 2005-04-23 removed token_trans.ML (some content moved to syn_ext.ML);
2005-04-16 wenzelm 2005-04-16 Syntax.mk_trfun;
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;
2004-05-29 wenzelm 2004-05-29 tuned _dummy_ofsort syntax;
2003-11-06 schirmer 2003-11-06 Records: - Record types are now by default printed with their type abbreviation instead of the list of all field types. This can be configured via the reference "print_record_type_abbr". - Simproc "record_upd_simproc" for simplification of multiple updates added (not enabled by default). - Tactic "record_split_simp_tac" to split and simplify records added. - Bug-fix and optimisation of "record_simproc". - "record_simproc" and "record_upd_simproc" are now sensitive to quick_and_dirty flag.
2003-07-02 nipkow 2003-07-02 Type antiquotations do not use the bracket syntax by default any longer.
2002-01-16 wenzelm 2002-01-16 GPLed;
2001-11-28 wenzelm 2001-11-28 support "_::foo" sort constraints;
2001-05-20 nipkow 2001-05-20 added (no)_type_brackets
2000-12-01 wenzelm 2000-12-01 no_brackets mode;
2000-06-14 wenzelm 2000-06-14 tuned tappl syntax;
2000-05-21 wenzelm 2000-05-21 added sort_of_term; export sortT;
1999-09-07 wenzelm 1999-09-07 logtypes: pretend "dummy" is one;
1999-07-06 wenzelm 1999-07-06 export term_of_typ;
1998-10-20 wenzelm 1998-10-20 no open;
1997-10-10 wenzelm 1997-10-10 added longid syntax;
1997-10-06 wenzelm 1997-10-06 fixed raw_term_sorts (again!); eliminated raise_ast;
1997-02-28 wenzelm 1997-02-28 term_of_... now mark class, tfree, tvar;
1997-02-24 wenzelm 1997-02-24 added "_" syntax for dummyT;
1997-02-06 wenzelm 1997-02-06 improved comments; raw_term_sorts: improved handling of sort constraints (consistency); added term_of_sort; renamed "_emptysort" to "_topsort"; preparations for marking of class idts;
1996-12-18 oheimb 1996-12-18 little improvement for the handling of sort constraints: two non-identical explicit constriants are considered equal if they give the same set in different enumerations, e.g. {term,ord,ord} = {ord,term}
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.
1994-12-08 clasohm 1994-12-08 changed Pure's grammar and the way types are converted to nonterminals
1994-10-12 wenzelm 1994-10-12 removed old comment;