| 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
|