| 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
|
| Tue, 14 Aug 2012 11:43:08 +0200 |
wenzelm |
support for 'typ' with explicit sort constraint;
|
file |
diff |
annotate
|
| Thu, 02 Aug 2012 12:36:54 +0200 |
wenzelm |
more official command specifications, including source position;
|
file |
diff |
annotate
|
| Thu, 02 Aug 2012 11:32:23 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 02 Aug 2012 00:15:32 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 02 Aug 2012 00:02:00 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Wed, 01 Aug 2012 23:33:26 +0200 |
wenzelm |
more standard bootstrapping of Pure outer syntax;
|
file |
diff |
annotate
|
| Tue, 10 Apr 2012 21:31:05 +0200 |
wenzelm |
static relevance of proof via syntax keywords;
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 21:46:45 +0200 |
wenzelm |
more general context command with auxiliary fixes/assumes etc.;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 23:26:35 +0100 |
wenzelm |
more explicit Toplevel.open_target/close_target;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 21:06:31 +0100 |
wenzelm |
optional 'includes' element for long theorem statements;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 17:25:35 +0100 |
wenzelm |
basic support for nested contexts including bundles;
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 20:00:13 +0100 |
wenzelm |
basic support for bundled declarations;
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 22:46:19 +0100 |
wenzelm |
more precise syntax;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 22:48:38 +0100 |
wenzelm |
eliminated odd 'finalconsts' / Theory.add_finals;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 21:20:23 +0100 |
wenzelm |
more abstract heading level;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 13:05:30 +0100 |
wenzelm |
define keywords early when processing the theory header, before running the body commands;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 22:08:53 +0100 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 19:02:34 +0100 |
wenzelm |
declare minor keywords via theory header;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 00:10:45 +0100 |
wenzelm |
some support for outer syntax keyword declarations within theory header;
|
file |
diff |
annotate
|
| Wed, 14 Mar 2012 17:52:38 +0100 |
wenzelm |
source positions for locale and class expressions;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 20:10:36 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 17:44:41 +0100 |
wenzelm |
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
|
file |
diff |
annotate
|
| Mon, 14 Nov 2011 16:52:19 +0100 |
wenzelm |
pass positions for named targets, for formal links in the document model;
|
file |
diff |
annotate
|
| Thu, 13 Oct 2011 11:45:33 +0200 |
wenzelm |
discontinued obsolete 'types' command;
|
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
|
| Sat, 13 Aug 2011 20:49:41 +0200 |
wenzelm |
simplified Toplevel.init_theory: discontinued special name argument;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 20:41:29 +0200 |
wenzelm |
simplified Toplevel.init_theory: discontinued special master argument;
|
file |
diff |
annotate
|
| Sat, 23 Jul 2011 16:37:17 +0200 |
wenzelm |
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
|
file |
diff |
annotate
|
| Tue, 12 Jul 2011 15:12:50 +0200 |
wenzelm |
added Parse.properties (again) -- allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 07:57:24 +0200 |
blanchet |
fixed typo in legacy feature message
|
file |
diff |
annotate
|
| Sun, 15 May 2011 17:06:35 +0200 |
wenzelm |
optional description for 'attribute_setup' and 'method_setup';
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 23:02:43 +0200 |
wenzelm |
more precise positions via binding;
|
file |
diff |
annotate
|
| Sat, 23 Apr 2011 13:53:09 +0200 |
wenzelm |
proper binding/report of defined simprocs;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:25:25 +0200 |
wenzelm |
prefer local name spaces;
|
file |
diff |
annotate
|
| Sat, 09 Apr 2011 23:29:50 +0200 |
wenzelm |
some position reports for 'translations';
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 22:59:52 +0200 |
wenzelm |
notation: proper markup for type constructor / constant;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 22:50:50 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 03 Apr 2011 21:59:33 +0200 |
wenzelm |
added Position.reports convenience;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 16:01:00 +0100 |
wenzelm |
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
|
file |
diff |
annotate
|
| Sun, 16 Jan 2011 14:57:14 +0100 |
wenzelm |
added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
|
file |
diff |
annotate
|
| Thu, 13 Jan 2011 17:34:45 +0100 |
wenzelm |
Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
|
file |
diff |
annotate
|
| Thu, 06 Jan 2011 21:06:18 +0100 |
ballarin |
Diagnostic command to show locale dependencies.
|
file |
diff |
annotate
|
| Sat, 18 Dec 2010 18:43:13 +0100 |
ballarin |
Add mixins to sublocale command.
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 18:10:37 +0100 |
wenzelm |
Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature);
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 17:43:54 +0100 |
wenzelm |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
file |
diff |
annotate
|
| Sun, 05 Dec 2010 14:02:16 +0100 |
wenzelm |
command 'notepad' replaces former 'example_proof';
|
file |
diff |
annotate
|
| Sat, 04 Dec 2010 21:26:55 +0100 |
wenzelm |
formal notepad without any result;
|
file |
diff |
annotate
|
| Sun, 28 Nov 2010 16:15:31 +0100 |
wenzelm |
added 'syntax_declaration' command;
|
file |
diff |
annotate
|
| Sun, 07 Nov 2010 16:39:03 +0100 |
wenzelm |
'example_proof' is treated as non-schematic statement with irrelevant proof (NB: even regular proofs can contain unreachable parts wrt. the graph of proof promises);
|
file |
diff |
annotate
|
| Sat, 06 Nov 2010 19:36:54 +0100 |
wenzelm |
mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;
|
file |
diff |
annotate
|
| Wed, 08 Sep 2010 13:22:24 +0200 |
haftmann |
removed ancient constdefs command
|
file |
diff |
annotate
|
| Mon, 06 Sep 2010 22:31:54 +0200 |
wenzelm |
discontinued obsolete ProofContext.prems_limit;
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 23:46:49 +0200 |
wenzelm |
moved Toplevel.run_command to Pure/PIDE/document.ML;
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 11:17:05 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 14:18:09 +0200 |
wenzelm |
discontinued obsolete 'global' and 'local' commands;
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 16:02:03 +0200 |
haftmann |
more convenient split of class modules: class and class_declaration
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 14:45:38 +0200 |
haftmann |
renamed Theory_Target to the more appropriate Named_Target
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 14:31:43 +0200 |
haftmann |
moved instantiation target formally to class_target.ML
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 12:30:48 +0200 |
haftmann |
moved overloading target formally to overloading.ML
|
file |
diff |
annotate
|
| Sat, 31 Jul 2010 21:14:20 +0200 |
ballarin |
Interpretation in proofs supports mixins.
|
file |
diff |
annotate
|
| Wed, 28 Jul 2010 00:13:26 +0200 |
wenzelm |
explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents;
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 23:01:42 +0200 |
wenzelm |
theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 22:00:26 +0200 |
wenzelm |
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
|
file |
diff |
annotate
|
| Sat, 24 Jul 2010 12:14:53 +0200 |
wenzelm |
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
|
file |
diff |
annotate
|