src/Pure/display.ML
2014-04-06 wenzelm 2014-04-06 more source positions;
2014-03-12 wenzelm 2014-03-12 tuned signature;
2014-03-11 wenzelm 2014-03-11 tuned signature;
2014-03-10 wenzelm 2014-03-10 abstract type Name_Space.table; clarified pretty_locale_deps: sort strings; clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;
2014-02-20 wenzelm 2014-02-20 clarified printing of undeclared hyps;
2013-05-16 wenzelm 2013-05-16 more system options as context-sensitive config options;
2013-03-30 wenzelm 2013-03-30 more item markup; tuned signature;
2013-03-30 wenzelm 2013-03-30 item markup for Proof_Context.pretty_fact; tuned signature;
2013-03-30 wenzelm 2013-03-30 obsolete, cf. Proof_Context.print_syntax;
2013-03-25 wenzelm 2013-03-25 tuned print_classes: more standard order, markup, formatting; uniform printing of minimal supersort/classrel;
2013-03-25 wenzelm 2013-03-25 tuned message;
2012-11-30 wenzelm 2012-11-30 print formal entities with markup;
2012-11-19 wenzelm 2012-11-19 theorem status about oracles/futures is no longer printed by default; renamed Proofterm/Thm.status_of to Proofterm/Thm.peek_status to emphasize its semantics;
2012-09-25 wenzelm 2012-09-25 added graph encode/decode operations; tuned signature;
2012-03-18 wenzelm 2012-03-18 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2011-04-18 wenzelm 2011-04-18 pass plain Proof.context for pretty printing;
2011-04-18 wenzelm 2011-04-18 simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;
2011-04-16 wenzelm 2011-04-16 prefer local name spaces; tuned signatures; tuned;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2010-09-06 wenzelm 2010-09-06 turned show_hyps and show_tags into proper configuration option;
2010-09-03 wenzelm 2010-09-03 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 wenzelm 2010-09-03 turned show_consts into proper configuration option;
2010-06-01 wenzelm 2010-06-01 arities: no need to maintain original codomain (cf. f795c1164708) -- completion happens in axclass.ML; misc tuning;
2010-04-25 wenzelm 2010-04-25 replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-18 wenzelm 2010-02-18 pretty_full_theory: proper Syntax.init_pretty_global;
2009-10-25 wenzelm 2009-10-25 eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 wenzelm 2009-10-25 conceal consts via name space, not tags;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 wenzelm 2009-10-24 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-08-28 wenzelm 2009-08-28 discontinued Display.pretty_ctyp/cterm etc.;
2009-08-28 wenzelm 2009-08-28 removed obsolete print_ctyp, print_cterm;
2009-07-25 wenzelm 2009-07-25 renamed structure Display_Goal to Goal_Display;
2009-07-23 wenzelm 2009-07-23 clarified pretty_goals, pretty_thm_aux: plain context; explicit pretty_goals_without_context, print_goals_without_context; tuned;
2009-07-21 wenzelm 2009-07-21 moved ProofContext.pretty_thm to Display.pretty_thm etc.; explicit old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.; removed some very old thm print operations;
2009-07-20 wenzelm 2009-07-20 moved pretty_goals etc. to Display_Goal (required by tracing tacticals); load display.ML after assumption.ML, to accomodate proper contextual theorem display;
2009-03-26 wenzelm 2009-03-26 pretty_thm_aux etc.: explicit show_status flag;
2009-03-24 wenzelm 2009-03-24 display derivation status of thms;
2009-03-10 wenzelm 2009-03-10 pretty_full_theory: no longer display name prefix -- naming is far more complex now;
2009-03-01 wenzelm 2009-03-01 replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already); minor tuning according to Isabelle coding conventions;
2009-02-11 kleing 2009-02-11 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-12-13 wenzelm 2008-12-13 Context.display_names;
2008-11-18 wenzelm 2008-11-18 tuned;
2008-11-15 wenzelm 2008-11-15 pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);
2008-09-22 wenzelm 2008-09-22 type thm: fully internal derivation, no longer exported;
2008-09-18 wenzelm 2008-09-18 simplified oracle interface;
2008-09-18 wenzelm 2008-09-18 added deriv.ML: Abstract derivations based on raw proof terms.
2008-06-20 haftmann 2008-06-20 type constructors now with markup
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-04-13 wenzelm 2008-04-13 tsig: removed unnecessary universal witness;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-27 wenzelm 2008-03-27 removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);
2007-11-11 wenzelm 2007-11-11 simplified Consts.dest;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-10-04 wenzelm 2007-10-04 replaced literal 'a by Name.aT;