| Fri, 25 Sep 2015 20:04:25 +0200 |
wenzelm |
less redundant output;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 19:54:51 +0200 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| Thu, 24 Sep 2015 23:33:29 +0200 |
wenzelm |
more explicit Defs.context: use proper name spaces as far as possible;
|
file |
diff |
annotate
|
| Wed, 23 Sep 2015 09:36:18 +0200 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Wed, 23 Sep 2015 09:30:12 +0200 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 22:42:48 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 20:21:53 +0200 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 18:56:25 +0200 |
wenzelm |
separate command 'print_definitions';
|
file |
diff |
annotate
|
| Sat, 15 Aug 2015 19:42:35 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Thu, 13 Aug 2015 11:05:19 +0200 |
wenzelm |
tuned signature, in accordance to sortBy in Scala;
|
file |
diff |
annotate
|
| Tue, 23 Dec 2014 20:46:42 +0100 |
wenzelm |
explicit message channels for "state", "information";
|
file |
diff |
annotate
|
| Tue, 22 Jul 2014 14:03:00 +0200 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Fri, 09 May 2014 22:04:50 +0200 |
wenzelm |
more position markup to help locating the query context, e.g. from "Info" dockable;
|
file |
diff |
annotate
|
| Wed, 07 May 2014 13:55:16 +0200 |
wenzelm |
print results as "state", to avoid intrusion into the source text;
|
file |
diff |
annotate
|
| Wed, 07 May 2014 11:50:30 +0200 |
wenzelm |
more emphatic output for Proof General;
|
file |
diff |
annotate
|
| Mon, 05 May 2014 17:14:46 +0200 |
wenzelm |
clarified print operations for "terms" and "theorems";
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 11:22:25 +0100 |
wenzelm |
more explicit treatment of verbose mode, which includes concealed entries;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 10:53:19 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 13 May 2013 12:40:17 +0200 |
wenzelm |
retain goal display options when printing error messages, to avoid breakdown for huge goals;
|
file |
diff |
annotate
|
| Wed, 03 Apr 2013 13:58:00 +0200 |
wenzelm |
tuned output -- less bullets;
|
file |
diff |
annotate
|
| Sat, 30 Mar 2013 13:40:19 +0100 |
wenzelm |
more item markup;
|
file |
diff |
annotate
|
| Mon, 19 Nov 2012 20:23:47 +0100 |
wenzelm |
theorem status about oracles/futures is no longer printed by default;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 20:35:24 +0200 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 20:23:00 +0200 |
wenzelm |
more proof method text position information;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 15:14:12 +0200 |
wenzelm |
more informative errors for 'proof' and 'apply' steps;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 14:02:02 +0200 |
wenzelm |
further attempts to unify/simplify goal output;
|
file |
diff |
annotate
|
| Tue, 28 Feb 2012 16:43:32 +0100 |
wenzelm |
display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
|
file |
diff |
annotate
|
| Wed, 26 Oct 2011 22:51:06 +0200 |
wenzelm |
more robust ML pretty printing (cf. b6c527c64789);
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 16:46:58 +0200 |
wenzelm |
improved default context for ML toplevel pretty-printing;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 22:04:07 +0200 |
wenzelm |
less verbosity in batch mode -- spam reduction and notable performance improvement;
|
file |
diff |
annotate
|
| Thu, 12 May 2011 16:23:13 +0200 |
wenzelm |
proper configuration options Proof_Context.debug and Proof_Context.verbose;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 16:00:11 +0100 |
wenzelm |
tuned markup;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 21:44:52 +0200 |
wenzelm |
tuned markup;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 22:02:11 +0100 |
wenzelm |
eliminated obsolete "internal" kind -- collapsed to unspecific "";
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 14:38:36 +0100 |
wenzelm |
print_theorems: suppress concealed (global) facts, unless "!" option is given;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:57:48 +0100 |
wenzelm |
modernized structure Proof_Display;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 16:52:16 +0200 |
wenzelm |
clarified pretty_goals, pretty_thm_aux: plain context;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 01:03:18 +0200 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 15:20:50 +0100 |
wenzelm |
pretty_rule/print_results: no thm status here -- it is potentially slow and mostly uninformative/confusing as long as proofs are still unfinished;
|
file |
diff |
annotate
|
| Sat, 21 Mar 2009 20:00:23 +0100 |
wenzelm |
removed obsolete pprint operations;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Fri, 12 Sep 2008 12:04:16 +0200 |
wenzelm |
more procise printing of fact names;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 22:20:16 +0200 |
wenzelm |
no pervasive bindings;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 18:01:24 +0200 |
wenzelm |
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);
|
file |
diff |
annotate
|
| Wed, 13 Aug 2008 20:57:31 +0200 |
wenzelm |
removed obsolete present_results;
|
file |
diff |
annotate
|
| Thu, 12 Jun 2008 16:41:58 +0200 |
wenzelm |
Facts.dest/export_static: content difference;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:43 +0200 |
wenzelm |
pprint: proper global context via Syntax.init_pretty_global;
|
file |
diff |
annotate
|
| Wed, 16 Apr 2008 21:53:04 +0200 |
wenzelm |
pretty_theorems: use proper PureThy.facts_of;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2008 22:40:07 +0100 |
wenzelm |
adapted to Context.thread_data interface;
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 16:04:30 +0100 |
wenzelm |
Facts.Named: include position;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:27:57 +0100 |
wenzelm |
renamed datatype thmref to Facts.ref, tuned interfaces;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| Tue, 08 May 2007 17:40:20 +0200 |
wenzelm |
tuned ProofDisplay.pretty_full_theory;
|
file |
diff |
annotate
|
| Sat, 17 Feb 2007 17:19:59 +0100 |
aspinall |
pretty_full_theory: expose in signature.
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:08:02 +0100 |
wenzelm |
moved ML context stuff to from Context to ML_Context;
|
file |
diff |
annotate
|