src/Pure/display.ML
2012-11-30 ago print formal entities with markup;
2012-11-19 ago theorem status about oracles/futures is no longer printed by default;
2012-09-25 ago added graph encode/decode operations;
2012-03-18 ago maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2011-06-09 ago tuned signature: Name.invent and Name.invent_names;
2011-04-18 ago pass plain Proof.context for pretty printing;
2011-04-18 ago simplified pretty printing context, which is only required for certain kernel operations;
2011-04-16 ago prefer local name spaces;
2011-04-16 ago Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2010-09-06 ago turned show_hyps and show_tags into proper configuration option;
2010-09-03 ago pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
2010-09-03 ago turned show_consts into proper configuration option;
2010-06-01 ago arities: no need to maintain original codomain (cf. f795c1164708) -- completion happens in axclass.ML;
2010-04-25 ago replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-18 ago pretty_full_theory: proper Syntax.init_pretty_global;
2009-10-25 ago eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 ago conceal consts via name space, not tags;
2009-10-24 ago renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 ago eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-09-30 ago eliminated redundant bindings;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-08-28 ago discontinued Display.pretty_ctyp/cterm etc.;
2009-08-28 ago removed obsolete print_ctyp, print_cterm;
2009-07-25 ago renamed structure Display_Goal to Goal_Display;
2009-07-23 ago clarified pretty_goals, pretty_thm_aux: plain context;
2009-07-21 ago moved ProofContext.pretty_thm to Display.pretty_thm etc.;
2009-07-20 ago moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
2009-03-26 ago pretty_thm_aux etc.: explicit show_status flag;
2009-03-24 ago display derivation status of thms;
2009-03-10 ago pretty_full_theory: no longer display name prefix -- naming is far more complex now;
2009-03-01 ago replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
2009-02-11 ago Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
2009-01-21 ago removed Ids;
2008-12-13 ago Context.display_names;
2008-11-18 ago tuned;
2008-11-15 ago pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);
2008-09-22 ago type thm: fully internal derivation, no longer exported;
2008-09-18 ago simplified oracle interface;
2008-09-18 ago added deriv.ML: Abstract derivations based on raw proof terms.
2008-06-20 ago type constructors now with markup
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 ago structure Display: less pervasive operations;
2008-04-13 ago tsig: removed unnecessary universal witness;
2008-04-12 ago rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-27 ago removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);
2007-11-11 ago simplified Consts.dest;
2007-10-09 ago generic Syntax.pretty/string_of operations;
2007-10-04 ago replaced literal 'a by Name.aT;
2007-09-30 ago print_theory: observe Markup.internal_property of consts, discontinued special treatment of internal names elsewhere;
2007-09-20 ago avoid Theory.rep_theory;
2007-07-08 ago thm tag: Markup.property list;
2007-07-07 ago pretty_goals_aux: subgoal markup;
2007-05-08 ago tuned;
2007-05-07 ago simplified DataFun interfaces;
2006-12-09 ago abbrevs: print original rhs;
2006-12-05 ago thm/prf: separate official name vs. additional tags;
2006-09-19 ago pretty_full_theory: suppress internal entities by default;
2006-07-27 ago removed obsolete pretty_thm_no_quote;
2006-07-26 ago moved pprint functions to Isar/proof_display.ML;