Tue, 08 Mar 2016 21:07:48 +0100 |
haftmann |
explicit record values for dictionary variables
|
file |
diff |
annotate
|
Thu, 03 Mar 2016 23:33:22 +0100 |
wenzelm |
simplified;
|
file |
diff |
annotate
|
Mon, 29 Feb 2016 20:35:06 +0100 |
wenzelm |
isabelle_process executable no longer supports writable heap images;
|
file |
diff |
annotate
|
Sun, 06 Sep 2015 22:14:52 +0200 |
haftmann |
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
|
file |
diff |
annotate
|
Wed, 28 Jan 2015 08:29:08 +0100 |
haftmann |
string printing conformant to both (S)ML and Isabelle/ML
|
file |
diff |
annotate
|
Fri, 09 Jan 2015 08:36:59 +0100 |
haftmann |
modernized and more uniform style
|
file |
diff |
annotate
|
Fri, 05 Dec 2014 19:35:36 +0100 |
haftmann |
allow multiple inheritance of targets
|
file |
diff |
annotate
|
Fri, 02 May 2014 21:18:50 +0200 |
haftmann |
enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)
|
file |
diff |
annotate
|
Thu, 01 May 2014 09:30:36 +0200 |
haftmann |
centralized upper/lowercase name mangling
|
file |
diff |
annotate
|
Thu, 27 Feb 2014 18:07:53 +0100 |
haftmann |
amended some slips, rolling back currently dysfunctional export minimimalisation for Scala
|
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
|
Sun, 23 Feb 2014 10:33:43 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
Sun, 23 Feb 2014 10:33:43 +0100 |
haftmann |
more fine-grain notion of export
|
file |
diff |
annotate
|
Sun, 23 Feb 2014 10:33:43 +0100 |
haftmann |
formal markup for public ingredients
|
file |
diff |
annotate
|
Sun, 23 Feb 2014 10:33:43 +0100 |
haftmann |
dropped long-unused option
|
file |
diff |
annotate
|
Fri, 21 Feb 2014 19:20:24 +0100 |
haftmann |
dropped dead code
|
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
|
Sat, 25 Jan 2014 23:50:49 +0100 |
haftmann |
more abstract declaration of unqualified constant names in code printing context
|
file |
diff |
annotate
|
Thu, 04 Jul 2013 08:52:44 +0200 |
haftmann |
explicit hint for domain of class parameters in instance statements
|
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
|
Fri, 24 May 2013 23:57:24 +0200 |
haftmann |
bookkeeping and input syntax for exact specification of names of symbols in generated code
|
file |
diff |
annotate
|
Fri, 15 Feb 2013 08:31:31 +0100 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
Wed, 13 Feb 2013 13:38:52 +0100 |
haftmann |
another attempt for a uniform abort on code generation errors
|
file |
diff |
annotate
|
Thu, 27 Dec 2012 21:01:08 +0100 |
haftmann |
more explicit name
|
file |
diff |
annotate
|
Sat, 17 Nov 2012 20:47:56 +0100 |
wenzelm |
more portable process exit;
|
file |
diff |
annotate
|
Wed, 07 Nov 2012 20:48:04 +0100 |
haftmann |
restored SML code check which got unintentionally broken: must explicitly check for error during compilation;
|
file |
diff |
annotate
|
Fri, 27 Jul 2012 22:26:38 +0200 |
haftmann |
evaluation: allow multiple code modules
|
file |
diff |
annotate
|
Tue, 05 Jun 2012 07:05:56 +0200 |
haftmann |
prefer records with speaking labels over deeply nested tuples
|
file |
diff |
annotate
|
Mon, 28 May 2012 13:38:07 +0200 |
haftmann |
dropped sort constraints on datatype specifications
|
file |
diff |
annotate
|
Thu, 19 Apr 2012 19:18:11 +0200 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
Thu, 19 Apr 2012 10:16:51 +0200 |
haftmann |
dropped dead code;
|
file |
diff |
annotate
|
Tue, 20 Sep 2011 09:30:19 +0200 |
bulwahn |
syntactic improvements and tuning names in the code generator due to Florian's code review
|
file |
diff |
annotate
|
Wed, 07 Sep 2011 13:51:32 +0200 |
bulwahn |
adding the body type as well to the code generation for constants as it is required for type annotations of constants
|
file |
diff |
annotate
|
Wed, 07 Sep 2011 13:51:30 +0200 |
bulwahn |
changing const type to pass along if typing annotations are necessary for disambigous terms
|
file |
diff |
annotate
|
Thu, 09 Jun 2011 23:30:18 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
Thu, 09 Jun 2011 14:16:12 +0200 |
bulwahn |
resolving an issue with class instances that are pseudo functions in the OCaml code serializer
|
file |
diff |
annotate
|
Thu, 09 Jun 2011 17:51:49 +0200 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
file |
diff |
annotate
|
Mon, 02 May 2011 10:50:09 +0200 |
bulwahn |
improving naming of fresh variables in OCaml serializer
|
file |
diff |
annotate
|
Sun, 13 Mar 2011 19:16:19 +0100 |
wenzelm |
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
|
file |
diff |
annotate
|
Sun, 13 Mar 2011 14:51:38 +0100 |
wenzelm |
allow spaces in executable names;
|
file |
diff |
annotate
|
Tue, 21 Dec 2010 08:40:39 +0100 |
haftmann |
program is separate argument to serializer
|
file |
diff |
annotate
|
Mon, 13 Dec 2010 22:54:47 +0100 |
haftmann |
separated dictionary weakning into separate type
|
file |
diff |
annotate
|
Thu, 09 Dec 2010 17:25:43 +0100 |
haftmann |
dictionary constants must permit explicit weakening of classes;
|
file |
diff |
annotate
|
Sat, 20 Nov 2010 00:53:26 +0100 |
wenzelm |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
file |
diff |
annotate
|
Sat, 04 Sep 2010 21:14:40 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
Sat, 04 Sep 2010 21:13:13 +0200 |
haftmann |
printing combinator for hierarchical programs
|
file |
diff |
annotate
|
Sat, 04 Sep 2010 21:10:48 +0200 |
haftmann |
dropped names from serializer interface
|
file |
diff |
annotate
|
Thu, 02 Sep 2010 19:08:48 +0200 |
haftmann |
hand out deresolver from serializer invocation
|
file |
diff |
annotate
|
Thu, 02 Sep 2010 16:14:13 +0200 |
haftmann |
swapped slip
|
file |
diff |
annotate
|
Thu, 02 Sep 2010 15:09:51 +0200 |
haftmann |
restored and added surpression of case combinators
|
file |
diff |
annotate
|
Thu, 02 Sep 2010 14:59:28 +0200 |
haftmann |
dropped superfluous presentation names
|
file |
diff |
annotate
|
Thu, 02 Sep 2010 14:36:49 +0200 |
haftmann |
manage statement selection for presentation wholly through markup
|
file |
diff |
annotate
|
Thu, 02 Sep 2010 13:58:16 +0200 |
haftmann |
formal markup of generated code for statements
|
file |
diff |
annotate
|
Thu, 02 Sep 2010 12:30:22 +0200 |
haftmann |
formal framework for presentation of selected statements
|
file |
diff |
annotate
|
Thu, 02 Sep 2010 10:33:13 +0200 |
haftmann |
dropped dead code; tuned
|
file |
diff |
annotate
|
Thu, 02 Sep 2010 10:29:48 +0200 |
haftmann |
use code_namespace module for SML and OCaml code
|
file |
diff |
annotate
|
Wed, 01 Sep 2010 08:52:49 +0200 |
haftmann |
tuned internally and made smlnj happy
|
file |
diff |
annotate
|
Tue, 31 Aug 2010 16:51:29 +0200 |
haftmann |
avoid strange special treatment of empty module names
|
file |
diff |
annotate
|
Tue, 31 Aug 2010 15:08:04 +0200 |
haftmann |
dropped single_module parameter
|
file |
diff |
annotate
|
Tue, 31 Aug 2010 14:21:06 +0200 |
haftmann |
record argument for serializers
|
file |
diff |
annotate
|
Tue, 31 Aug 2010 13:55:54 +0200 |
haftmann |
removed serializer interface redundancies
|
file |
diff |
annotate
|
Tue, 31 Aug 2010 13:29:38 +0200 |
haftmann |
more coherent naming of syntax data structures
|
file |
diff |
annotate
|
Tue, 31 Aug 2010 13:15:35 +0200 |
haftmann |
Code_Printer.tuplify
|
file |
diff |
annotate
|
Tue, 31 Aug 2010 13:08:58 +0200 |
haftmann |
dropped legacy interfaces
|
file |
diff |
annotate
|
Mon, 30 Aug 2010 16:33:06 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Mon, 30 Aug 2010 16:31:38 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Mon, 30 Aug 2010 16:21:47 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Mon, 30 Aug 2010 16:17:10 +0200 |
haftmann |
eliminated some obscure higher-order arguments
|
file |
diff |
annotate
|
Mon, 30 Aug 2010 16:00:41 +0200 |
haftmann |
width is a formal parameter of serialization
|
file |
diff |
annotate
|
Mon, 30 Aug 2010 09:28:02 +0200 |
haftmann |
code checking: compiler invocation happens in same directory as generated file -- avoid problem with different path representations on cygwin
|
file |
diff |
annotate
|
Thu, 26 Aug 2010 20:14:24 +0200 |
haftmann |
proper passing of optional module name
|
file |
diff |
annotate
|
Thu, 26 Aug 2010 13:50:58 +0200 |
haftmann |
tuned serializer interface
|
file |
diff |
annotate
|
Thu, 26 Aug 2010 12:30:43 +0200 |
haftmann |
private version of commas, cf. printmode
|
file |
diff |
annotate
|
Thu, 29 Jul 2010 12:28:45 +0200 |
haftmann |
rebinding ref is illegal
|
file |
diff |
annotate
|
Sat, 24 Jul 2010 18:08:41 +0200 |
haftmann |
another refinement chapter in the neverending numeral story
|
file |
diff |
annotate
|
Wed, 14 Jul 2010 15:08:02 +0200 |
haftmann |
use generic description slot for formal code checking
|
file |
diff |
annotate
|
Wed, 14 Jul 2010 14:53:44 +0200 |
haftmann |
formal slot for code checker
|
file |
diff |
annotate
|
Wed, 14 Jul 2010 14:20:47 +0200 |
haftmann |
check without explicit path
|
file |
diff |
annotate
|
Thu, 08 Jul 2010 16:41:57 +0200 |
haftmann |
dropped ancient in-place compilation of SML
|
file |
diff |
annotate
|
Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
checking generated code for various target languages
|
file |
diff |
annotate
|
Thu, 17 Jun 2010 15:59:47 +0200 |
haftmann |
more precise code
|
file |
diff |
annotate
|
Thu, 17 Jun 2010 11:33:04 +0200 |
haftmann |
transitive superclasses were also only a misunderstanding
|
file |
diff |
annotate
|
Thu, 17 Jun 2010 10:57:00 +0200 |
haftmann |
formal introduction of transitive superclasses
|
file |
diff |
annotate
|
Thu, 17 Jun 2010 10:51:38 +0200 |
haftmann |
dropped obscure type argument weakening mapping -- was only a misunderstanding
|
file |
diff |
annotate
|
Tue, 15 Jun 2010 11:38:40 +0200 |
haftmann |
drop function definitions of combinators
|
file |
diff |
annotate
|
Tue, 15 Jun 2010 08:32:32 +0200 |
haftmann |
formal introduction of case cong
|
file |
diff |
annotate
|
Mon, 07 Jun 2010 13:42:38 +0200 |
haftmann |
more consistent naming aroud type classes and instances
|
file |
diff |
annotate
|
Tue, 01 Jun 2010 13:52:11 +0200 |
haftmann |
brackify_infix etc.: no break before infix operator -- eases survival in Scala
|
file |
diff |
annotate
|
Thu, 29 Apr 2010 15:00:43 +0200 |
haftmann |
fixed underscore typo
|
file |
diff |
annotate
|
Wed, 28 Apr 2010 16:56:19 +0200 |
haftmann |
exported print_tuple
|
file |
diff |
annotate
|
Fri, 19 Feb 2010 11:06:22 +0100 |
haftmann |
context theorem is optional
|
file |
diff |
annotate
|
Fri, 22 Jan 2010 13:38:28 +0100 |
haftmann |
code literals: distinguish numeral classes by different entries
|
file |
diff |
annotate
|
Mon, 04 Jan 2010 14:09:57 +0100 |
haftmann |
dropped redundant name declarations
|
file |
diff |
annotate
|
Wed, 23 Dec 2009 11:32:08 +0100 |
haftmann |
take care for destructive print mode properly using dedicated pretty builders
|
file |
diff |
annotate
|
Fri, 11 Dec 2009 20:32:49 +0100 |
haftmann |
default_code_width is now proper theory data
|
file |
diff |
annotate
|
Tue, 08 Dec 2009 14:31:19 +0100 |
haftmann |
simplified notion of empty module name
|
file |
diff |
annotate
|
Mon, 07 Dec 2009 16:27:48 +0100 |
haftmann |
split off evaluation mechanisms in separte module Code_Eval
|
file |
diff |
annotate
|
Fri, 04 Dec 2009 18:19:32 +0100 |
haftmann |
signatures for generated code; tuned
|
file |
diff |
annotate
|
Thu, 12 Nov 2009 15:10:27 +0100 |
haftmann |
accomplish mutual recursion between fun and inst
|
file |
diff |
annotate
|
Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
Wed, 14 Oct 2009 12:04:16 +0200 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
Wed, 14 Oct 2009 11:56:44 +0200 |
haftmann |
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
|
file |
diff |
annotate
|
Mon, 12 Oct 2009 15:46:38 +0200 |
haftmann |
intro_base_names combinator
|
file |
diff |
annotate
|
Mon, 12 Oct 2009 12:19:19 +0200 |
haftmann |
factored out Code_Printer.aux_params
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
Tue, 21 Jul 2009 15:44:31 +0200 |
haftmann |
integrated add_triv_classes into evaluation stack
|
file |
diff |
annotate
|
Fri, 03 Jul 2009 16:51:07 +0200 |
haftmann |
cleaned up fundamental iml term functions
|
file |
diff |
annotate
|
Tue, 30 Jun 2009 17:33:30 +0200 |
haftmann |
all variable names are optional
|
file |
diff |
annotate
|
Tue, 30 Jun 2009 14:54:00 +0200 |
haftmann |
simplified binding concept
|
file |
diff |
annotate
|
Tue, 23 Jun 2009 12:09:30 +0200 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
| base
|