src/Pure/Isar/proof_display.ML
2016-04-06 wenzelm 2016-04-06 clarified modules; tuned signature;
2016-01-16 wenzelm 2016-01-16 tuned message;
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-09-25 wenzelm 2015-09-25 less redundant output;
2015-09-25 wenzelm 2015-09-25 proper context;
2015-09-24 wenzelm 2015-09-24 more explicit Defs.context: use proper name spaces as far as possible;
2015-09-23 wenzelm 2015-09-23 tuned output;
2015-09-23 wenzelm 2015-09-23 tuned output;
2015-09-22 wenzelm 2015-09-22 tuned signature;
2015-09-22 wenzelm 2015-09-22 tuned output;
2015-09-22 wenzelm 2015-09-22 separate command 'print_definitions';
2015-08-15 wenzelm 2015-08-15 clarified context;
2015-08-13 wenzelm 2015-08-13 tuned signature, in accordance to sortBy in Scala;
2014-12-23 wenzelm 2014-12-23 explicit message channels for "state", "information"; separate state_message_color;
2014-07-22 wenzelm 2014-07-22 tuned messages;
2014-05-09 wenzelm 2014-05-09 more position markup to help locating the query context, e.g. from "Info" dockable;
2014-05-07 wenzelm 2014-05-07 print results as "state", to avoid intrusion into the source text; print new local theory (again);
2014-05-07 wenzelm 2014-05-07 more emphatic output for Proof General;
2014-05-05 wenzelm 2014-05-05 clarified print operations for "terms" and "theorems";
2014-03-15 wenzelm 2014-03-15 more explicit treatment of verbose mode, which includes concealed entries;
2014-02-26 wenzelm 2014-02-26 tuned signature;
2013-05-13 wenzelm 2013-05-13 retain goal display options when printing error messages, to avoid breakdown for huge goals;
2013-04-03 wenzelm 2013-04-03 tuned output -- less bullets;
2013-03-30 wenzelm 2013-03-30 more item markup; tuned signature;
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-10-16 wenzelm 2012-10-16 tuned messages;
2012-10-16 wenzelm 2012-10-16 more proof method text position information;
2012-10-16 wenzelm 2012-10-16 more informative errors for 'proof' and 'apply' steps; more Seq.result operations;
2012-10-16 wenzelm 2012-10-16 further attempts to unify/simplify goal output;
2012-02-28 wenzelm 2012-02-28 display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
2011-10-26 wenzelm 2011-10-26 more robust ML pretty printing (cf. b6c527c64789);
2011-08-17 wenzelm 2011-08-17 improved default context for ML toplevel pretty-printing;
2011-08-13 wenzelm 2011-08-13 less verbosity in batch mode -- spam reduction and notable performance improvement; clarified Proof_Display.print_consts;
2011-05-12 wenzelm 2011-05-12 proper configuration options Proof_Context.debug and Proof_Context.verbose; discontinued alias Proof.verbose = Proof_Context.verbose;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-01-14 wenzelm 2011-01-14 tuned markup;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-09 wenzelm 2010-09-09 tuned markup;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2009-11-12 wenzelm 2009-11-12 eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-11-08 wenzelm 2009-11-08 print_theorems: suppress concealed (global) facts, unless "!" option is given;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_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 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-03-26 wenzelm 2009-03-26 pretty_rule/print_results: no thm status here -- it is potentially slow and mostly uninformative/confusing as long as proofs are still unfinished;
2009-03-21 wenzelm 2009-03-21 removed obsolete pprint operations; some explicit pp operations for toplevel pretty printing;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-09-12 wenzelm 2008-09-12 more procise printing of fact names;
2008-09-02 wenzelm 2008-09-02 no pervasive bindings; removed theory_results and related hook; print_results: ignore empty/internal kind -- like former theory_results;
2008-09-02 wenzelm 2008-09-02 pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
2008-08-13 wenzelm 2008-08-13 removed obsolete present_results; added theory_results, which is subject to hooks (formerly in present.ML);
2008-06-12 wenzelm 2008-06-12 Facts.dest/export_static: content difference; tuned;
2008-05-18 wenzelm 2008-05-18 pprint: proper global context via Syntax.init_pretty_global;
2008-04-16 wenzelm 2008-04-16 pretty_theorems: use proper PureThy.facts_of;
2008-03-26 wenzelm 2008-03-26 adapted to Context.thread_data interface;
2008-03-20 wenzelm 2008-03-20 Facts.Named: include position;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;