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
|
Fri, 23 Aug 2013 20:35:50 +0200 |
wenzelm |
added Theory.setup convenience;
|
file |
diff |
annotate
|
Fri, 23 Aug 2013 19:53:27 +0200 |
wenzelm |
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
|
file |
diff |
annotate
|
Sun, 23 Jun 2013 21:16:07 +0200 |
haftmann |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file |
diff |
annotate
|
Sun, 23 Jun 2013 21:16:06 +0200 |
haftmann |
more appropriate cutting of input syntax
|
file |
diff |
annotate
|
Fri, 27 Jul 2012 22:26:38 +0200 |
haftmann |
evaluation: allow multiple code modules
|
file |
diff |
annotate
|
Thu, 19 Apr 2012 19:18:11 +0200 |
haftmann |
dropped dead code
|
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
|
Thu, 15 Mar 2012 20:07:00 +0100 |
wenzelm |
prefer formally checked @{keyword} parser;
|
file |
diff |
annotate
|
Thu, 15 Mar 2012 19:02:34 +0100 |
wenzelm |
declare minor keywords via theory header;
|
file |
diff |
annotate
|
Wed, 29 Feb 2012 23:09:06 +0100 |
wenzelm |
clarified module Thy_Load;
|
file |
diff |
annotate
|
Wed, 09 Nov 2011 21:36:18 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
Wed, 26 Oct 2011 22:50:40 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 02 Sep 2011 19:29:36 +0200 |
haftmann |
avoid "Code" as structure name
|
file |
diff |
annotate
|
Fri, 01 Jul 2011 15:16:03 +0200 |
wenzelm |
proper @{binding} antiquotations (relevant for formal references);
|
file |
diff |
annotate
|
Mon, 27 Jun 2011 16:53:31 +0200 |
wenzelm |
ML antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 15:25:25 +0200 |
wenzelm |
prefer local name spaces;
|
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, 09 Jan 2011 21:33:41 +0100 |
wenzelm |
reverted 08240feb69c7 -- breaks positions of reports;
|
file |
diff |
annotate
|
Sat, 08 Jan 2011 17:14:48 +0100 |
wenzelm |
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
|
file |
diff |
annotate
|
Tue, 21 Dec 2010 21:05:50 +0100 |
wenzelm |
more robust ML antiquotations -- allow original tokens without adjacent whitespace;
|
file |
diff |
annotate
|
Tue, 21 Dec 2010 09:29:33 +0100 |
haftmann |
evaluator separating static and dynamic operations
|
file |
diff |
annotate
|
Tue, 21 Dec 2010 09:19:37 +0100 |
haftmann |
tuned naming
|
file |
diff |
annotate
|
Tue, 21 Dec 2010 09:18:29 +0100 |
haftmann |
evaluator separating static and dynamic operations
|
file |
diff |
annotate
|
Tue, 21 Dec 2010 08:40:39 +0100 |
haftmann |
program is separate argument to serializer
|
file |
diff |
annotate
|
Fri, 17 Dec 2010 18:24:44 +0100 |
haftmann |
avoid slightly odd Conv.tap_thy
|
file |
diff |
annotate
|
Wed, 15 Dec 2010 09:47:12 +0100 |
haftmann |
simplified evaluation function names
|
file |
diff |
annotate
|
Thu, 09 Dec 2010 17:25:43 +0100 |
haftmann |
tuned names
|
file |
diff |
annotate
|
Thu, 09 Dec 2010 09:58:33 +0100 |
haftmann |
tracing of term to be evaluated
|
file |
diff |
annotate
|
Fri, 26 Nov 2010 22:33:21 +0100 |
haftmann |
keep type variable arguments of datatype constructors in bookkeeping
|
file |
diff |
annotate
|
Fri, 26 Nov 2010 12:03:18 +0100 |
haftmann |
globbing constant expressions use more idiomatic underscore rather than star
|
file |
diff |
annotate
|
Mon, 08 Nov 2010 10:56:48 +0100 |
haftmann |
corrected slip: must keep constant map, not type map; tuned code
|
file |
diff |
annotate
|
Mon, 08 Nov 2010 10:43:24 +0100 |
haftmann |
constructors to datatypes in code_reflect can be globbed; dropped unused code
|
file |
diff |
annotate
|
Wed, 03 Nov 2010 10:44:53 +0100 |
haftmann |
polyml_as_definition does not require explicit dependencies on external ML files
|
file |
diff |
annotate
|
Fri, 29 Oct 2010 11:35:28 +0200 |
haftmann |
actually pass "verbose" argument
|
file |
diff |
annotate
|
Thu, 28 Oct 2010 22:04:00 +0200 |
wenzelm |
use Exn.interruptible_capture to keep user-code interruptible (Exn.capture not immediately followed by Exn.release here);
|
file |
diff |
annotate
|
Tue, 26 Oct 2010 11:20:14 +0200 |
haftmann |
Code_Runtime.trace
|
file |
diff |
annotate
|
Fri, 01 Oct 2010 22:44:36 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
Fri, 01 Oct 2010 17:06:49 +0200 |
haftmann |
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
|
file |
diff |
annotate
|
Fri, 01 Oct 2010 17:23:26 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
Fri, 01 Oct 2010 11:46:09 +0200 |
haftmann |
added polyml_as_definition -- using external SML files as substitute for proper definitions -- only for polyml!
|
file |
diff |
annotate
|
Tue, 21 Sep 2010 15:46:06 +0200 |
haftmann |
reject term variables explicitly
|
file |
diff |
annotate
|
Mon, 20 Sep 2010 08:53:37 +0200 |
haftmann |
made smlnj happy
|
file |
diff |
annotate
|
Fri, 17 Sep 2010 10:00:01 +0200 |
haftmann |
closures preserve static serializer context for static evaluation; tuned
|
file |
diff |
annotate
|
Fri, 17 Sep 2010 08:41:07 +0200 |
haftmann |
made sml/nj happy
|
file |
diff |
annotate
|
Thu, 16 Sep 2010 16:51:34 +0200 |
haftmann |
dynamic and static value computation; built-in evaluation of propositions
|
file |
diff |
annotate
|
Wed, 15 Sep 2010 16:56:31 +0200 |
haftmann |
proper interface for code_reflect
|
file |
diff |
annotate
|
Wed, 15 Sep 2010 15:40:36 +0200 |
haftmann |
Code_Runtime.value, corresponding to ML_Context.value; tuned
|
file |
diff |
annotate
|
Wed, 15 Sep 2010 15:31:32 +0200 |
haftmann |
code_eval renamed to code_runtime
|
file |
diff |
annotate
| base
|