| Mon, 03 Jun 2019 13:28:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 14:12:44 +0100 |
wenzelm |
clarified signature: more types;
|
file |
diff |
annotate
|
| Tue, 27 Nov 2018 21:07:39 +0100 |
wenzelm |
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
|
file |
diff |
annotate
|
| Wed, 31 Oct 2018 15:53:32 +0100 |
wenzelm |
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
|
file |
diff |
annotate
|
| Thu, 25 Oct 2018 21:29:08 +0200 |
wenzelm |
clarified ML position: proper markup for def/ref scopes (see also 162a4c2e97bc);
|
file |
diff |
annotate
|
| Mon, 27 Aug 2018 20:43:01 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 27 Aug 2018 14:42:24 +0200 |
wenzelm |
support named ML environments, notably "Isabelle", "SML";
|
file |
diff |
annotate
|
| Sun, 01 Jul 2018 12:38:37 +0200 |
wenzelm |
discontinued pending_shyps: too much complication due to lazy facts;
|
file |
diff |
annotate
|
| Fri, 29 Jun 2018 15:54:41 +0200 |
wenzelm |
disallow pending hyps;
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 22:07:21 +0100 |
wenzelm |
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 19:18:49 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 16 Feb 2018 18:25:35 +0100 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 18:59:33 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2016 11:51:42 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 21 Jun 2016 11:03:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2016 12:02:38 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2016 11:40:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 12 May 2016 22:06:18 +0200 |
wenzelm |
common entity definitions within a global or local theory context;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 15:42:52 +0200 |
wenzelm |
unfold is subject to unfold_abs_def (still inactive);
|
file |
diff |
annotate
|
| Mon, 18 Apr 2016 20:24:19 +0200 |
wenzelm |
prefer internal attribute source;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 12:13:11 +0200 |
wenzelm |
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 20:51:37 +0200 |
wenzelm |
clarified modules -- simplified bootstrap;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 17:14:27 +0200 |
wenzelm |
removed redundant Position.set_range -- already done in Position.range;
|
file |
diff |
annotate
|
| Wed, 02 Mar 2016 19:43:31 +0100 |
wenzelm |
support for ML_exception_debugger;
|
file |
diff |
annotate
|
| Tue, 15 Dec 2015 16:01:57 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 20:58:09 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 18:45:46 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 16:36:26 +0100 |
wenzelm |
clarified type Token.src: plain token list, with usual implicit value assignment;
|
file |
diff |
annotate
|
| Fri, 30 Oct 2015 17:14:30 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
| Sun, 18 Oct 2015 21:30:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2015 16:03:11 +0200 |
wenzelm |
proper attribute;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 17:36:46 +0200 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 17:19:27 +0200 |
wenzelm |
tuned output -- avoid empty quites and extra breaks;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2015 19:56:51 +0200 |
wenzelm |
more uniform "verbose" option to print name space;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 12:24:56 +0100 |
wenzelm |
more abstract type Input.source;
|
file |
diff |
annotate
|
| Wed, 12 Nov 2014 10:30:59 +0100 |
wenzelm |
more careful ML source positions, for improved PIDE markup;
|
file |
diff |
annotate
|
| Tue, 11 Nov 2014 20:11:38 +0100 |
wenzelm |
more careful ML source positions, for improved PIDE markup;
|
file |
diff |
annotate
|
| Tue, 11 Nov 2014 18:16:25 +0100 |
wenzelm |
more position information, e.g. relevant for errors in generated ML source;
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
| Wed, 05 Nov 2014 20:20:57 +0100 |
wenzelm |
explicit type Keyword.keywords;
|
file |
diff |
annotate
|
| Sat, 01 Nov 2014 19:47:48 +0100 |
wenzelm |
tuned signature (see ab2483fad861);
|
file |
diff |
annotate
|
| Wed, 27 Aug 2014 12:32:42 +0200 |
wenzelm |
tuned signature -- prefer quasi-abstract Symbol_Pos.source;
|
file |
diff |
annotate
|
| Mon, 25 Aug 2014 12:58:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 21 Aug 2014 22:48:39 +0200 |
wenzelm |
tuned signature -- define some elementary operations earlier;
|
file |
diff |
annotate
|
| Thu, 21 Aug 2014 10:07:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 16:20:14 +0200 |
wenzelm |
more informative Token.Fact: retain name of dynamic fact (without selection);
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 14:28:11 +0200 |
wenzelm |
localized command 'method_setup' and 'attribute_setup';
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 12:33:21 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 12:13:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 11:55:09 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 13 Aug 2014 13:57:55 +0200 |
wenzelm |
localized attribute definitions;
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 11:06:36 +0200 |
wenzelm |
refined context visibility again (amending f5f9fad3321c, 8e3e004f1c31): avoid spurious warning due to global config options;
|
file |
diff |
annotate
|
| Sun, 06 Apr 2014 16:36:28 +0200 |
wenzelm |
more source positions;
|
file |
diff |
annotate
|
| Sun, 06 Apr 2014 15:43:45 +0200 |
wenzelm |
more source positions;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 12:35:39 +0200 |
wenzelm |
some shortcuts for chunks, which sometimes avoid bulky string output;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 17:12:40 +0100 |
wenzelm |
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 19:03:02 +0100 |
wenzelm |
proper configuration option "ML_print_depth";
|
file |
diff |
annotate
|