| Tue, 01 Sep 2015 23:10:23 +0200 |
wenzelm |
thread context for exceptions from forks, e.g. relevant when printing errors;
|
file |
diff |
annotate
|
| Mon, 17 Aug 2015 16:27:12 +0200 |
wenzelm |
explicit debug flag for ML compiler;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:52:14 +0100 |
wenzelm |
clarified context;
|
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
|
| Fri, 19 Dec 2014 20:32:54 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 12:56:06 +0100 |
wenzelm |
proper exception for internal program failure, not user-error;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 12:36:50 +0100 |
wenzelm |
tuned;
|
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
|
| Fri, 05 Dec 2014 19:35:36 +0100 |
haftmann |
allow multiple inheritance of targets
|
file |
diff |
annotate
|
| Thu, 09 Oct 2014 22:43:48 +0200 |
haftmann |
more foundational definition for predicate even
|
file |
diff |
annotate
|
| Thu, 09 Oct 2014 16:47:56 +0200 |
haftmann |
formally completeted set of experimental static evaluation functions
|
file |
diff |
annotate
|
| Sun, 05 Oct 2014 20:30:57 +0200 |
haftmann |
basic support for fully static evaluator generation without dynamic compiler invocation
|
file |
diff |
annotate
|
| Sun, 05 Oct 2014 20:30:56 +0200 |
haftmann |
split dynamic from static context
|
file |
diff |
annotate
|
| Sun, 29 Jun 2014 18:02:18 +0200 |
haftmann |
modernized diagnostic options
|
file |
diff |
annotate
|
| Thu, 15 May 2014 16:38:31 +0200 |
haftmann |
syntactic means to prevent accidental mixup of static and dynamic context
|
file |
diff |
annotate
|
| Thu, 15 May 2014 16:38:29 +0200 |
haftmann |
dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
|
file |
diff |
annotate
|
| Fri, 09 May 2014 08:13:26 +0200 |
haftmann |
normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>;
|
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
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 17:39:03 +0100 |
wenzelm |
clarifed module name;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 16:16:28 +0100 |
wenzelm |
clarified modules;
|
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, 26 Feb 2014 11:57:52 +0100 |
haftmann |
prefer proof context over background theory
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 10:33:43 +0100 |
haftmann |
keep only identifiers public which are explicitly requested or demanded by dependencies
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 10:33:43 +0100 |
haftmann |
explicit option for "open" code generation
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 16:33:54 +0100 |
wenzelm |
more formal markup;
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 16:09:04 +0100 |
haftmann |
reduced prominence of "permissive code generation"
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 23:50:49 +0100 |
haftmann |
less clumsy namespace
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 23:50:49 +0100 |
haftmann |
prefer explicit code symbol type over ad-hoc name mangling
|
file |
diff |
annotate
|