| Fri, 27 Jun 2014 16:04:56 +0200 |
wenzelm |
command 'print_term_bindings' supersedes 'print_binds';
|
file |
diff |
annotate
|
| Fri, 06 Jun 2014 19:19:46 +0200 |
haftmann |
dropped obscure and unused ad-hoc before_exit hook for named targets
|
file |
diff |
annotate
|
| Wed, 07 May 2014 12:59:15 +0200 |
wenzelm |
discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
|
file |
diff |
annotate
|
| Wed, 07 May 2014 10:42:19 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 06 May 2014 23:08:18 +0200 |
wenzelm |
clarified print_state, which goes back to TTY loop before Proof General, and before separate print_context;
|
file |
diff |
annotate
|
| Mon, 05 May 2014 17:27:42 +0200 |
wenzelm |
uniform Toplevel.print for all proof commands;
|
file |
diff |
annotate
|
| Mon, 05 May 2014 17:14:46 +0200 |
wenzelm |
clarified print operations for "terms" and "theorems";
|
file |
diff |
annotate
|
| Mon, 05 May 2014 16:30:19 +0200 |
wenzelm |
more print operations;
|
file |
diff |
annotate
|
| Tue, 22 Apr 2014 12:03:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 19 Apr 2014 17:23:05 +0200 |
wenzelm |
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 14:59:36 +0200 |
wenzelm |
more uniform ML/document antiquotations;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 10:28:08 +0200 |
wenzelm |
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 17:56:13 +0100 |
wenzelm |
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 13:18:10 +0100 |
wenzelm |
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 11:06:39 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 10:45:03 +0100 |
wenzelm |
tuned signature;
|
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
|
| Sat, 15 Mar 2014 10:14:42 +0100 |
wenzelm |
clarified print_local_facts;
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 21:58:48 +0100 |
wenzelm |
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 17:02:05 +0100 |
wenzelm |
more explicit markup and explanation of the improper status of 'back', following the AFP style-guide;
|
file |
diff |
annotate
|
| Sun, 09 Mar 2014 17:37:34 +0100 |
wenzelm |
more formal read_root;
|
file |
diff |
annotate
|
| Sun, 09 Mar 2014 17:08:31 +0100 |
wenzelm |
simplified / modernized hide commands: proper outer parsers and PIDE markup via check;
|
file |
diff |
annotate
|
| Sat, 08 Mar 2014 21:08:10 +0100 |
wenzelm |
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 10:40:04 +0100 |
wenzelm |
more explicit method reports;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 10:40:13 +0100 |
wenzelm |
method language markup, e.g. relevant to prevent outer keyword completion;
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 14:34:18 +0100 |
wenzelm |
modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
|
file |
diff |
annotate
|
| Mon, 10 Feb 2014 22:08:18 +0100 |
wenzelm |
discontinued axiomatic 'classes', 'classrel', 'arities';
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 18:34:05 +0100 |
wenzelm |
prefer self-contained user-space tool;
|
file |
diff |
annotate
|
| Mon, 30 Sep 2013 11:20:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 04 Sep 2013 15:27:24 +0200 |
wenzelm |
some explicit indication of Proof General legacy;
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 13:09:15 +0200 |
wenzelm |
cases: more position information and PIDE markup;
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 11:58:34 +0200 |
wenzelm |
more liberal 'case' syntax: allow parentheses without arguments;
|
file |
diff |
annotate
|
| Sun, 07 Jul 2013 18:34:29 +0200 |
wenzelm |
discontinued command 'print_drafts';
|
file |
diff |
annotate
|
| Sun, 07 Jul 2013 17:30:16 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Mon, 24 Jun 2013 17:17:17 +0200 |
wenzelm |
back to keyword 'pr' :: diag as required for ProofGeneral command line -- reject this TTY command in Isabelle/jEdit by other means;
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 21:23:36 +0200 |
wenzelm |
proper diagnostic command 'print_state';
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| Fri, 17 May 2013 20:53:28 +0200 |
wenzelm |
renamed 'print_configs' to 'print_options';
|
file |
diff |
annotate
|
| Tue, 14 May 2013 12:31:11 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Mon, 13 May 2013 13:23:13 +0200 |
wenzelm |
option "goals_limit", with more uniform description;
|
file |
diff |
annotate
|
| Tue, 23 Apr 2013 11:14:50 +0200 |
haftmann |
target-sensitive user-level commands interpretation and sublocale
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 15:30:19 +0200 |
wenzelm |
more standard module name Axclass (according to file name);
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 15:29:25 +0200 |
wenzelm |
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 12:56:26 +0200 |
wenzelm |
just one syntax category "mixfix" -- check structure annotation semantically;
|
file |
diff |
annotate
|
| Fri, 05 Apr 2013 20:54:55 +0200 |
wenzelm |
tuned signature -- agree with markup terminology;
|
file |
diff |
annotate
|
| Sat, 30 Mar 2013 14:57:06 +0100 |
wenzelm |
added 'print_defn_rules' command;
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 16:38:17 +0100 |
wenzelm |
discontinued obsolete 'axioms' command;
|
file |
diff |
annotate
|
| Wed, 27 Feb 2013 17:32:17 +0100 |
wenzelm |
discontinued redundant 'use' command;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2013 16:16:22 +0100 |
wenzelm |
tuned -- less indirection;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 14:43:28 +0100 |
wenzelm |
tuned command descriptions;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 13:54:43 +0100 |
wenzelm |
refined outer syntax 'help' command;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 21:26:36 +0200 |
wenzelm |
more informative errors for 'also' and 'finally';
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 17:47:23 +0200 |
wenzelm |
clarified defer/prefer: more specific errors;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 15:14:12 +0200 |
wenzelm |
more informative errors for 'proof' and 'apply' steps;
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 14:23:33 +0200 |
wenzelm |
tuned pretty_locale/print_locale, with more basic pretty_locale_deps based on that;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 13:08:51 +0200 |
wenzelm |
command 'use' is legacy;
|
file |
diff |
annotate
|
| Sun, 26 Aug 2012 21:46:50 +0200 |
wenzelm |
theory def/ref position reports, which enable hyperlinks etc.;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 12:47:49 +0200 |
wenzelm |
clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
|
file |
diff |
annotate
|