src/Tools/Code/code_ml.ML
Fri, 24 Apr 2020 13:16:40 +0000 haftmann opaque export does not work as expected in presence of dependent instances
Sun, 16 Jun 2019 16:40:57 +0000 haftmann more correct indicator
Fri, 22 Mar 2019 18:04:52 +0100 wenzelm workaround for the sake of Windows;
Wed, 20 Mar 2019 20:15:30 +0100 wenzelm access OCaml tools and libraries via ISABELLE_OCAMLFIND;
Thu, 14 Mar 2019 13:54:31 +0000 haftmann dedicated environment setting for ocaml environment: ISABELLE_OPAM_ROOT is always present even if no envionrment is available
Sun, 10 Mar 2019 15:16:45 +0000 haftmann migrated from Nums to Zarith as library for OCaml integer arithmetic
Fri, 25 Jan 2019 22:13:48 +0000 haftmann prefer proper strings in OCaml
Thu, 10 Jan 2019 12:07:05 +0000 haftmann explicit model concerning files of generated code
Tue, 30 Oct 2018 15:45:24 +0100 wenzelm clarified signature;
Tue, 24 Apr 2018 14:17:58 +0000 haftmann proper datatype for 8-bit characters
Thu, 14 Dec 2017 18:42:39 +0100 haftmann dedicated case option for code generation to Scala
Thu, 03 Aug 2017 12:49:58 +0200 haftmann tuned
Thu, 03 Aug 2017 12:49:57 +0200 haftmann work around weakness in export calculation when generating OCaml code
Tue, 14 Jun 2016 20:48:41 +0200 haftmann explicit resolution of ambiguous dictionaries
Sun, 29 May 2016 14:43:17 +0200 haftmann do not export abstract constructors in code_reflect
Mon, 18 Apr 2016 20:56:11 +0200 haftmann environment variable check has become pointless after 771b8ad5c7fc
Wed, 13 Apr 2016 14:25:02 +0200 wenzelm tuned;
Wed, 16 Mar 2016 11:45:25 +0100 wenzelm less physical "logic" argument, with option -l like "isabelle console" etc.;
Thu, 10 Mar 2016 12:11:50 +0100 wenzelm isabelle_process is superseded by "isabelle process" tool;
Wed, 09 Mar 2016 21:01:22 +0100 wenzelm merged
Wed, 09 Mar 2016 19:30:09 +0100 wenzelm isabelle.Build uses ML_Process directly;
Tue, 08 Mar 2016 21:07:48 +0100 haftmann explicit record values for dictionary variables
Thu, 03 Mar 2016 23:33:22 +0100 wenzelm simplified;
Mon, 29 Feb 2016 20:35:06 +0100 wenzelm isabelle_process executable no longer supports writable heap images;
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;
Wed, 28 Jan 2015 08:29:08 +0100 haftmann string printing conformant to both (S)ML and Isabelle/ML
Fri, 09 Jan 2015 08:36:59 +0100 haftmann modernized and more uniform style
Fri, 05 Dec 2014 19:35:36 +0100 haftmann allow multiple inheritance of targets
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)
Thu, 01 May 2014 09:30:36 +0200 haftmann centralized upper/lowercase name mangling
Thu, 27 Feb 2014 18:07:53 +0100 haftmann amended some slips, rolling back currently dysfunctional export minimimalisation for Scala
Sun, 23 Feb 2014 10:33:43 +0100 haftmann keep only identifiers public which are explicitly requested or demanded by dependencies
Sun, 23 Feb 2014 10:33:43 +0100 haftmann explicit option for "open" code generation
Sun, 23 Feb 2014 10:33:43 +0100 haftmann tuned
Sun, 23 Feb 2014 10:33:43 +0100 haftmann more fine-grain notion of export
Sun, 23 Feb 2014 10:33:43 +0100 haftmann formal markup for public ingredients
Sun, 23 Feb 2014 10:33:43 +0100 haftmann dropped long-unused option
Fri, 21 Feb 2014 19:20:24 +0100 haftmann dropped dead code
Sat, 25 Jan 2014 23:50:49 +0100 haftmann less clumsy namespace
Sat, 25 Jan 2014 23:50:49 +0100 haftmann prefer explicit code symbol type over ad-hoc name mangling
Sat, 25 Jan 2014 23:50:49 +0100 haftmann more abstract declaration of unqualified constant names in code printing context
Thu, 04 Jul 2013 08:52:44 +0200 haftmann explicit hint for domain of class parameters in instance statements
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
Fri, 24 May 2013 23:57:24 +0200 haftmann bookkeeping and input syntax for exact specification of names of symbols in generated code
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
Wed, 13 Feb 2013 13:38:52 +0100 haftmann another attempt for a uniform abort on code generation errors
Thu, 27 Dec 2012 21:01:08 +0100 haftmann more explicit name
Sat, 17 Nov 2012 20:47:56 +0100 wenzelm more portable process exit;
Wed, 07 Nov 2012 20:48:04 +0100 haftmann restored SML code check which got unintentionally broken: must explicitly check for error during compilation;
Fri, 27 Jul 2012 22:26:38 +0200 haftmann evaluation: allow multiple code modules
Tue, 05 Jun 2012 07:05:56 +0200 haftmann prefer records with speaking labels over deeply nested tuples
Mon, 28 May 2012 13:38:07 +0200 haftmann dropped sort constraints on datatype specifications
Thu, 19 Apr 2012 19:18:11 +0200 haftmann dropped dead code
Thu, 19 Apr 2012 10:16:51 +0200 haftmann dropped dead code;
Tue, 20 Sep 2011 09:30:19 +0200 bulwahn syntactic improvements and tuning names in the code generator due to Florian's code review
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
Wed, 07 Sep 2011 13:51:30 +0200 bulwahn changing const type to pass along if typing annotations are necessary for disambigous terms
Thu, 09 Jun 2011 23:30:18 +0200 wenzelm merged
Thu, 09 Jun 2011 14:16:12 +0200 bulwahn resolving an issue with class instances that are pseudo functions in the OCaml code serializer
Thu, 09 Jun 2011 17:51:49 +0200 wenzelm simplified Name.variant -- discontinued builtin fold_map;
less more (0) -100 -60 tip