src/Pure/Syntax/printer.ML
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;
2000-09-07 wenzelm 2000-09-07 internalize error "insufficient syntax for prefix application";
2000-03-15 wenzelm 2000-03-15 use Pretty.str / Pretty.raw_str;
1999-06-04 wenzelm 1999-06-04 print "..." variable;
1999-03-09 wenzelm 1999-03-09 token translation: real;
1999-02-12 wenzelm 1999-02-12 tuned pretty format lookup;
1999-02-11 wenzelm 1999-02-11 proper handling of print_mode wrt. Pretty.sym;
1999-01-29 oheimb 1999-01-29 moved print_mode to ROOT.ML
1998-10-20 wenzelm 1998-10-20 no open; handle multiple trfuns;
1998-03-09 wenzelm 1998-03-09 Symbol.output;
1997-12-28 wenzelm 1997-12-28 renamed Symtab.null to Symtab.empty;
1997-11-05 wenzelm 1997-11-05 print translation: added show_sorts argument;
1997-10-09 wenzelm 1997-10-09 changed preference order of prtab entries;
1997-10-06 wenzelm 1997-10-06 added sort_to_ast; eliminated raise_ast;
1997-04-04 wenzelm 1997-04-04 fixed diagnostic output of print modes;
1997-03-31 wenzelm 1997-03-31 simple_ast_of: fixed handling of loose Bounds;
1997-02-28 wenzelm 1997-02-28 split ast_of_term(T); ast_of_term now marks frees; added token translation support;
1997-01-13 wenzelm 1997-01-13 improved error msg;
1996-12-13 wenzelm 1996-12-13 removed chartrans_of; added typed print translations; error msg for _appl(C) loop;