src/Pure/Syntax/printer.ML
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-12-04 wenzelm 2010-12-04 added Syntax.pretty_priority;
2010-09-06 wenzelm 2010-09-06 more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
2010-09-05 wenzelm 2010-09-05 turned show_brackets into proper configuration option; Sign.certify/type_check: dropped Syntax.pp_show_brackets, which is hard to hold up due to Pretty.pp and not even present in the regular end-user type check;
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-09-03 wenzelm 2010-09-03 turned eta_contract into proper configuration option;
2010-09-03 wenzelm 2010-09-03 turned show_structs into proper configuration option;
2010-09-03 wenzelm 2010-09-03 turned show_all_types into proper configuration option;
2010-09-03 wenzelm 2010-09-03 treat show_free_types as plain ML option, without the extras of global default and registration in the attribute name space -- NB: 'print_configs' only shows the latter;
2010-09-03 wenzelm 2010-09-03 more explicit Config.declare vs. Config.declare_global;
2010-09-03 wenzelm 2010-09-03 turned show_no_free_types into proper configuration option show_free_types, with flipped polarity;
2010-09-02 wenzelm 2010-09-02 turned show_question_marks into proper configuration option; show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname; tuned;
2010-07-20 wenzelm 2010-07-20 eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that; tuned some error messages;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-03-03 wenzelm 2010-03-03 mark_atoms: more precise treatment of SynExt.standard_token_markers vs. syntax consts;
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-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-01-19 wenzelm 2009-01-19 removed Ids;
2008-04-17 wenzelm 2008-04-17 token translations: context dependent, result Pretty.T; added Markup.fixed (analogous to Markup.const); tuned;
2007-11-11 wenzelm 2007-11-11 replaced extend_prtabs by update_prtabs (absorb duplicates);
2007-11-10 wenzelm 2007-11-10 remove_prtabs: tuned, avoid excessive garbage;
2007-09-17 wenzelm 2007-09-17 avoid direct access to print_mode;
2007-07-23 wenzelm 2007-07-23 eliminated transform_failure (to avoid critical section for main transactions);
2007-07-09 wenzelm 2007-07-09 type output = string indicates raw system output;
2007-07-07 wenzelm 2007-07-07 pretty: markup for syntax/name of authentic consts; datatype symb: String (potential markup) vs. Space (no markup);
2007-07-07 wenzelm 2007-07-07 simplified pretty token metric: type int;
2006-12-11 wenzelm 2006-12-11 advanced translation functions: Proof.context;
2006-12-10 wenzelm 2006-12-10 support printing of idtdummy;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-08 wenzelm 2006-04-08 pretty: late externing of consts (support authentic syntax);
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-06 wenzelm 2006-02-06 TableFun: renamed xxx_multi to xxx_list; tuned;
2006-01-31 wenzelm 2006-01-31 advanced translations: Context.generic;
2005-11-09 wenzelm 2005-11-09 tuned;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-13 wenzelm 2005-09-13 replaced TRANSLATION_FAIL by EXCEPTION;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-31 haftmann 2005-08-31 introduced AList.*
2005-08-29 wenzelm 2005-08-29 use AList operations;
2005-06-29 wenzelm 2005-06-29 proper treatment of advanced trfuns: pass thy argument; transform_failure in translation functions: TRANSLATION_FAIL; removed obsolete '*** INSUFFICIENT SYNTAX FOR PREFIX APPLICATION ***';
2005-05-17 wenzelm 2005-05-17 tuned;
2005-04-23 wenzelm 2005-04-23 SynExt.standard_token_markers
2005-04-17 wenzelm 2005-04-17 tuned;
2005-04-16 wenzelm 2005-04-16 tuned extend_prtabs; added remove_prtabs;
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-20 wenzelm 2004-06-20 tuned pp;
2004-05-29 wenzelm 2004-05-29 added pp_show_brackets; support unbreakable blocks;
2004-05-21 wenzelm 2004-05-21 string_of_vname moved to term.ML;
2004-05-01 wenzelm 2004-05-01 tuned;
2003-08-29 skalberg 2003-08-29 Added show_all_types flag, such that all type information in the term is made explicit.
2002-01-16 wenzelm 2002-01-16 GPLed;
2001-11-24 wenzelm 2001-11-24 Symtab.merge_multi'; tuned;
2001-11-20 wenzelm 2001-11-20 prefer later trfuns;
2001-10-16 wenzelm 2001-10-16 be more careful about token class markers;