| Wed, 27 Mar 2019 22:15:36 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 27 Mar 2019 21:58:30 +0100 |
wenzelm |
export_code/check_code formally updates the theory -- this opens further possibilities concerning Generated_Files;
|
file |
diff |
annotate
|
| Wed, 27 Mar 2019 20:07:53 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 15:16:45 +0000 |
haftmann |
migrated from Nums to Zarith as library for OCaml integer arithmetic
|
file |
diff |
annotate
|
| Sat, 02 Feb 2019 15:52:14 +0100 |
wenzelm |
clarified signature: Path.T as in Generated_Files;
|
file |
diff |
annotate
|
| Sun, 20 Jan 2019 17:15:47 +0000 |
haftmann |
more conventional parsing of code_stmts antiquotation
|
file |
diff |
annotate
|
| Sun, 20 Jan 2019 17:14:35 +0000 |
haftmann |
more conventional syntax for code_stmts antiquotation
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 18:33:53 +0000 |
haftmann |
canonical operation to typeset generated code makes dedicated environment obsolete
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 13:58:12 +0100 |
wenzelm |
clarified message;
|
file |
diff |
annotate
|
| Sun, 13 Jan 2019 20:25:41 +0100 |
wenzelm |
information with hyperlink to "isabelle-export:";
|
file |
diff |
annotate
|
| Sun, 13 Jan 2019 19:03:16 +0100 |
wenzelm |
regular export with implicit compression: result is uncompressed;
|
file |
diff |
annotate
|
| Sun, 13 Jan 2019 18:48:25 +0100 |
wenzelm |
clarified -- removed pointless Parse.!!!;
|
file |
diff |
annotate
|
| Sun, 13 Jan 2019 18:40:26 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 10 Jan 2019 12:07:08 +0000 |
haftmann |
optional code export as theory export
|
file |
diff |
annotate
|
| Thu, 10 Jan 2019 12:07:05 +0000 |
haftmann |
explicit model concerning files of generated code
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sat, 29 Dec 2018 09:28:28 +0000 |
haftmann |
more correct handling of symbols for includes
|
file |
diff |
annotate
|
| Thu, 20 Dec 2018 12:55:45 +0000 |
haftmann |
proper attach mechanism for any kind of symbols, not just constants
|
file |
diff |
annotate
|
| Thu, 20 Dec 2018 12:40:24 +0000 |
haftmann |
disregard historic keyword
|
file |
diff |
annotate
|
| Thu, 18 Jan 2018 21:41:30 +0100 |
wenzelm |
clarified access to antiquotation options;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2018 15:40:12 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 14 Dec 2017 18:42:39 +0100 |
haftmann |
dedicated case option for code generation to Scala
|
file |
diff |
annotate
|
| Fri, 01 Sep 2017 12:47:23 +0200 |
wenzelm |
more PIDE markup;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2017 22:27:03 +0100 |
haftmann |
ML antiquotation for generated computations
|
file |
diff |
annotate
|
| Thu, 26 Jan 2017 16:06:19 +0100 |
haftmann |
tuned structure and terminology
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
optional timing for code generator conversions
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified proof context vs. background theory
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified naming conventions and code for code evaluation sandwiches
|
file |
diff |
annotate
|
| Mon, 18 Apr 2016 20:56:11 +0200 |
haftmann |
environment variable check has become pointless after 771b8ad5c7fc
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Mon, 07 Mar 2016 21:33:41 +0100 |
wenzelm |
tuned -- more standard operations;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Thu, 05 Feb 2015 13:01:12 +0100 |
haftmann |
dropped obsolete external entrance point
|
file |
diff |
annotate
|
| Thu, 05 Feb 2015 13:01:12 +0100 |
haftmann |
explicit error message for non-existing targets
|
file |
diff |
annotate
|
| Sat, 24 Jan 2015 16:42:37 +0100 |
wenzelm |
more direct Output.output;
|
file |
diff |
annotate
|
| Fri, 09 Jan 2015 08:37:00 +0100 |
haftmann |
prefer option for default code printing width
|
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
|
| Thu, 04 Dec 2014 16:51:54 +0100 |
haftmann |
tuned module structure
|
file |
diff |
annotate
|
| Thu, 04 Dec 2014 16:51:54 +0100 |
haftmann |
tuned data structures
|
file |
diff |
annotate
|
| Thu, 04 Dec 2014 16:51:54 +0100 |
haftmann |
tuned target inheritance bookkeeping: ancestry is always fully maintained at current entry using canonical merge;
|
file |
diff |
annotate
|
| Thu, 04 Dec 2014 16:51:54 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 04 Dec 2014 16:51:54 +0100 |
haftmann |
tuned names
|
file |
diff |
annotate
|
| Wed, 03 Dec 2014 14:04:38 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
| Wed, 05 Nov 2014 20:20:57 +0100 |
wenzelm |
explicit type Keyword.keywords;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 20:18:27 +0200 |
wenzelm |
tuned signature according to Scala version -- prefer explicit argument;
|
file |
diff |
annotate
|
| 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
|
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
|
| 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:35 +0200 |
haftmann |
optional case enforcement
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 17:39:03 +0100 |
wenzelm |
clarifed module name;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 11:27:09 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 09 Mar 2014 16:37:56 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 12:10:19 +0100 |
wenzelm |
tuned signature -- more uniform check_type_name/read_type_name;
|
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
|
| 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
|
| Sun, 09 Feb 2014 21:37:27 +0100 |
haftmann |
dropped legacy finally
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 19:50:38 +0100 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 16:33:54 +0100 |
wenzelm |
more formal markup;
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 08:23:19 +0100 |
haftmann |
tuned storage of code identifiers
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 16:09:04 +0100 |
haftmann |
reduced prominence of "permissive code generation"
|
file |
diff |
annotate
|
| Sun, 26 Jan 2014 16:23:46 +0100 |
haftmann |
more suitable names, without any notion of "activating"
|
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 |
immediate "activation" of const syntax at declaration time
|
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 syntax passing
|
file |
diff |
annotate
|
| Sat, 11 Jan 2014 08:10:12 +0100 |
haftmann |
dropped legacy alias feature
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 01:05:48 +0100 |
haftmann |
fundamental treatment of undefined vs. universally partial replaces code_abort
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 01:05:46 +0100 |
haftmann |
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
|
file |
diff |
annotate
|
| Mon, 07 Oct 2013 17:55:01 +0200 |
wenzelm |
proper warning at run time, not in the parser;
|
file |
diff |
annotate
|
| Thu, 05 Sep 2013 18:05:02 +0200 |
haftmann |
check explicit module names for conformity
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 22:31:34 +0200 |
wenzelm |
proper PIDE markup for codegen arguments;
|
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
|
| Sat, 15 Jun 2013 17:19:23 +0200 |
haftmann |
more consistent parsing and reading of classes and type constructors
|
file |
diff |
annotate
|
| Wed, 29 May 2013 10:47:42 +0200 |
wenzelm |
make SML/NJ happy;
|
file |
diff |
annotate
|
| Sun, 26 May 2013 21:05:03 +0200 |
wenzelm |
tuned;
|
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, 24 May 2013 23:57:24 +0200 |
haftmann |
use generic data for code symbols for unified "code_printing" syntax for custom serialisations
|
file |
diff |
annotate
|
| Sun, 19 May 2013 20:15:00 +0200 |
haftmann |
tuned, including signature
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 15:30:19 +0200 |
wenzelm |
more standard module name Axclass (according to file name);
|
file |
diff |
annotate
|
| Tue, 08 Jan 2013 12:39:39 +0100 |
wenzelm |
tuned -- prefer high-level Table.merge with its slightly more conservative update;
|
file |
diff |
annotate
|
| Fri, 27 Jul 2012 22:26:38 +0200 |
haftmann |
evaluation: allow multiple code modules
|
file |
diff |
annotate
|
| Sat, 21 Jul 2012 20:01:16 +0200 |
haftmann |
also consider current working directory (cf. 3a5a5a992519)
|
file |
diff |
annotate
|
| Thu, 19 Jul 2012 22:21:59 +0200 |
haftmann |
export code relatively to master directory
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 10:16:51 +0200 |
haftmann |
dropped dead code;
|
file |
diff |
annotate
|
| Fri, 23 Mar 2012 20:32:43 +0100 |
wenzelm |
tuned;
|
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
|
| Thu, 23 Feb 2012 15:49:40 +0100 |
wenzelm |
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 16:40:22 +0200 |
bulwahn |
avoid "Code" as structure name (cf. 3bc39cfe27fe)
|
file |
diff |
annotate
|
| Sat, 16 Jul 2011 20:52:41 +0200 |
wenzelm |
moved bash operations to Isabelle_System (cf. Scala version);
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 22:20:49 +0200 |
wenzelm |
document antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
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 14:51:38 +0100 |
wenzelm |
allow spaces in executable names;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 13:57:20 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 15:15:55 +0100 |
haftmann |
tuned names
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 10:20:33 +0100 |
haftmann |
only depend on exisiting statements
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 08:40:39 +0100 |
haftmann |
evaluator separating static and dynamic operations
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 07:45:04 +0100 |
haftmann |
more explicit structure for serializer invocation
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 14:44:00 +0100 |
wenzelm |
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
|
file |
diff |
annotate
|
| Fri, 01 Oct 2010 11:46:09 +0200 |
haftmann |
check whole target hierarchy for existing reserved symbols
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 09:14:37 +0200 |
haftmann |
consider quick_and_dirty option before loading theory
|
file |
diff |
annotate
|
| Fri, 24 Sep 2010 14:03:44 +0200 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 13:23:22 +0200 |
haftmann |
reverted cs 07549694e2f1 -- use re-printing with current print mode instead after code assembly, avoid Latex.output_typewriter
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 11:29:22 +0200 |
haftmann |
shifted abstraction over imperative print mode
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 10:37:28 +0200 |
haftmann |
improved and tuned external codegen tool
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 09:21:49 +0200 |
haftmann |
closures separate serializer initialization from serializer invocation as far as appropriate
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 17:31:51 +0200 |
haftmann |
added code_stmts antiquotation from doc-src/more_antiquote.ML
|
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 14:59:28 +0200 |
haftmann |
dropped superfluous presentation names
|
file |
diff |
annotate
|