| Sun, 24 Oct 2021 21:19:55 +0200 |
wenzelm |
more markup;
|
file |
diff |
annotate
|
| Sun, 24 Oct 2021 20:25:51 +0200 |
wenzelm |
clarified name, syntax, messages;
|
file |
diff |
annotate
|
| Sun, 24 Oct 2021 16:43:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 24 Oct 2021 16:38:13 +0200 |
wenzelm |
ML antiquotations to instantiate types/terms/props;
|
file |
diff |
annotate
|
| Thu, 21 Oct 2021 18:10:51 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 20:25:33 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 20:04:28 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 16:45:10 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
| base
|
| Fri, 16 Apr 2021 23:16:00 +0200 |
wenzelm |
support for conditional ML text;
|
file |
diff |
annotate
|
| Fri, 09 Apr 2021 22:06:59 +0200 |
wenzelm |
support for ML special forms: modified evaluation similar to Scheme;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2019 17:21:30 +0200 |
wenzelm |
added ML antiquotation @{oracle_name};
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 15:15:21 +0100 |
wenzelm |
mark for isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 21:49:06 +0100 |
wenzelm |
support for isabelle update -u control_cartouches;
|
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
|
| Thu, 21 Jun 2018 14:49:21 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 16 Dec 2017 12:16:40 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 18:59:33 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 15:46:35 +0100 |
wenzelm |
more embedded cartouche arguments;
|
file |
diff |
annotate
|
| Sun, 18 Dec 2016 12:32:20 +0100 |
wenzelm |
more permissive syntax;
|
file |
diff |
annotate
|
| Sun, 24 Jul 2016 16:48:39 +0200 |
haftmann |
text antiquotation for locales (similar to classes)
|
file |
diff |
annotate
|
| Wed, 01 Jun 2016 15:01:43 +0200 |
wenzelm |
support rat numerals via special antiquotation syntax;
|
file |
diff |
annotate
|
| Mon, 23 May 2016 21:30:30 +0200 |
wenzelm |
embedded content may be delimited via cartouches;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 13:54:02 +0200 |
wenzelm |
simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 13:35:08 +0200 |
wenzelm |
clarified bootstrap of @{make_string} -- avoid query on ML environment;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 19:48:54 +0200 |
wenzelm |
clarified conditional compilation;
|
file |
diff |
annotate
|
| Thu, 17 Mar 2016 16:56:44 +0100 |
wenzelm |
@{make_string} is available during Pure bootstrap;
|
file |
diff |
annotate
|
| Sun, 24 Jan 2016 15:02:29 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 06 Jan 2016 00:04:15 +0100 |
wenzelm |
added ML antiquotation @{method};
|
file |
diff |
annotate
|
| Sat, 07 Nov 2015 13:13:23 +0100 |
wenzelm |
less confusing markup;
|
file |
diff |
annotate
|
| Sat, 07 Nov 2015 12:53:22 +0100 |
wenzelm |
added @{undefined} with somewhat undefined symbol;
|
file |
diff |
annotate
|
| Sat, 07 Nov 2015 00:28:42 +0100 |
wenzelm |
ML cartouches via control antiquotation;
|
file |
diff |
annotate
|
| Thu, 10 Sep 2015 17:32:30 +0200 |
wenzelm |
removed obsolete undocumented feature;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 17:18:48 +0200 |
wenzelm |
formal Theory.check, with markup and completion;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 16:00:19 +0200 |
wenzelm |
more position information and PIDE markup for command keywords;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 16:43:49 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Wed, 25 Mar 2015 14:39:40 +0100 |
wenzelm |
semantic completion for @{system_option};
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2015 23:35:41 +0100 |
wenzelm |
added Proof_Context.cterm_of/ctyp_of convenience;
|
file |
diff |
annotate
|
| Wed, 10 Dec 2014 19:24:54 +0100 |
wenzelm |
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
|
file |
diff |
annotate
|
| Mon, 08 Dec 2014 22:42:12 +0100 |
wenzelm |
expand ML cartouches to Input.source;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 12:24:56 +0100 |
wenzelm |
more abstract type Input.source;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 16:55:43 +0100 |
wenzelm |
added ML antiquotation @{apply n} or @{apply n(k)};
|
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 17:43:50 +0100 |
wenzelm |
tuned;
|
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, 08 Oct 2014 17:09:07 +0200 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file |
diff |
annotate
|
| Wed, 08 Oct 2014 13:55:43 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 27 Aug 2014 12:32:07 +0200 |
wenzelm |
added ML antiquotation @{source} for Symbol_Pos.source;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 14:59:36 +0200 |
wenzelm |
more uniform ML/document antiquotations;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 14:15:48 +0200 |
wenzelm |
more positions and markup;
|
file |
diff |
annotate
|
| Fri, 04 Apr 2014 13:12:16 +0200 |
wenzelm |
tuned white space;
|
file |
diff |
annotate
|
| Fri, 04 Apr 2014 12:07:48 +0200 |
wenzelm |
added ML antiquotation @{print};
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 18:12:08 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 16:16:28 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|