src/Tools/Code/code_target.ML
Fri, 27 Jan 2017 22:27:03 +0100 haftmann ML antiquotation for generated computations
Thu, 26 Jan 2017 16:06:19 +0100 haftmann tuned structure and terminology
Thu, 26 May 2016 15:27:50 +0200 haftmann optional timing for code generator conversions
Thu, 26 May 2016 15:27:50 +0200 haftmann clarified proof context vs. background theory
Thu, 26 May 2016 15:27:50 +0200 haftmann clarified naming conventions and code for code evaluation sandwiches
Mon, 18 Apr 2016 20:56:11 +0200 haftmann environment variable check has become pointless after 771b8ad5c7fc
Wed, 13 Apr 2016 18:01:05 +0200 wenzelm eliminated "xname" and variants;
Mon, 07 Mar 2016 21:33:41 +0100 wenzelm tuned -- more standard operations;
Mon, 07 Mar 2016 21:09:28 +0100 wenzelm File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword};
Thu, 05 Feb 2015 13:01:12 +0100 haftmann dropped obsolete external entrance point
Thu, 05 Feb 2015 13:01:12 +0100 haftmann explicit error message for non-existing targets
Sat, 24 Jan 2015 16:42:37 +0100 wenzelm more direct Output.output;
Fri, 09 Jan 2015 08:37:00 +0100 haftmann prefer option for default code printing width
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
Thu, 04 Dec 2014 16:51:54 +0100 haftmann tuned module structure
Thu, 04 Dec 2014 16:51:54 +0100 haftmann tuned data structures
Thu, 04 Dec 2014 16:51:54 +0100 haftmann tuned target inheritance bookkeeping: ancestry is always fully maintained at current entry using canonical merge;
Thu, 04 Dec 2014 16:51:54 +0100 haftmann tuned
Thu, 04 Dec 2014 16:51:54 +0100 haftmann tuned names
Wed, 03 Dec 2014 14:04:38 +0100 wenzelm tuned signature;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Fri, 07 Nov 2014 16:36:55 +0100 wenzelm plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
Wed, 05 Nov 2014 20:20:57 +0100 wenzelm explicit type Keyword.keywords;
Tue, 12 Aug 2014 20:18:27 +0200 wenzelm tuned signature according to Scala version -- prefer explicit argument;
Thu, 12 Jun 2014 18:02:39 +0200 haftmann formal variable name: IVar NONE is strictly spoken not supported on lhs of function definitions, e.g. in Scala
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>;
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:35 +0200 haftmann optional case enforcement
Tue, 18 Mar 2014 17:39:03 +0100 wenzelm clarifed module name;
Tue, 18 Mar 2014 11:27:09 +0100 wenzelm tuned signature;
Sun, 09 Mar 2014 16:37:56 +0100 wenzelm tuned signature;
Thu, 06 Mar 2014 12:10:19 +0100 wenzelm tuned signature -- more uniform check_type_name/read_type_name;
Thu, 27 Feb 2014 18:07:53 +0100 haftmann amended some slips, rolling back currently dysfunctional export minimimalisation for Scala
Wed, 26 Feb 2014 11:57:52 +0100 haftmann prefer proof context over background theory
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, 09 Feb 2014 21:37:27 +0100 haftmann dropped legacy finally
Mon, 03 Feb 2014 19:50:38 +0100 wenzelm merged;
Mon, 03 Feb 2014 16:33:54 +0100 wenzelm more formal markup;
Mon, 03 Feb 2014 08:23:19 +0100 haftmann tuned storage of code identifiers
Thu, 30 Jan 2014 16:09:04 +0100 haftmann reduced prominence of "permissive code generation"
Sun, 26 Jan 2014 16:23:46 +0100 haftmann more suitable names, without any notion of "activating"
Sat, 25 Jan 2014 23:50:49 +0100 haftmann less clumsy namespace
Sat, 25 Jan 2014 23:50:49 +0100 haftmann immediate "activation" of const syntax at declaration time
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 syntax passing
Sat, 11 Jan 2014 08:10:12 +0100 haftmann dropped legacy alias feature
Wed, 01 Jan 2014 01:05:48 +0100 haftmann fundamental treatment of undefined vs. universally partial replaces code_abort
Wed, 01 Jan 2014 01:05:46 +0100 haftmann explicit distinction between empty code equations and no code equations, including convenient declaration attributes
Mon, 07 Oct 2013 17:55:01 +0200 wenzelm proper warning at run time, not in the parser;
Thu, 05 Sep 2013 18:05:02 +0200 haftmann check explicit module names for conformity
Tue, 30 Jul 2013 22:31:34 +0200 wenzelm proper PIDE markup for codegen arguments;
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
Sun, 23 Jun 2013 21:16:06 +0200 haftmann more appropriate cutting of input syntax
Sat, 15 Jun 2013 17:19:23 +0200 haftmann more consistent parsing and reading of classes and type constructors
Wed, 29 May 2013 10:47:42 +0200 wenzelm make SML/NJ happy;
Sun, 26 May 2013 21:05:03 +0200 wenzelm tuned;
Fri, 24 May 2013 23:57:24 +0200 haftmann bookkeeping and input syntax for exact specification of names of symbols in generated code
less more (0) -100 -60 tip