Tue, 04 Apr 2023 16:06:12 +0200 |
stuebinm |
code_target: create subdirectories for export_code file
|
file |
diff |
annotate
|
Tue, 03 Jan 2023 16:05:07 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Thu, 23 Jun 2022 21:50:32 +0200 |
wenzelm |
more scalable generated files and code export, using Bytes.T;
|
file |
diff |
annotate
|
Mon, 06 Dec 2021 15:34:54 +0100 |
wenzelm |
discontinued old-style {* verbatim *} tokens;
|
file |
diff |
annotate
|
Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
Fri, 21 May 2021 12:29:29 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Mon, 07 Dec 2020 16:09:06 +0100 |
wenzelm |
more accurate markup (refining 1c59b555ac4a);
|
file |
diff |
annotate
|
Tue, 27 Oct 2020 22:34:37 +0100 |
wenzelm |
clarified signature: overloaded "+" for Path.append;
|
file |
diff |
annotate
|
Mon, 05 Oct 2020 21:15:58 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Mon, 17 Aug 2020 13:16:42 +0200 |
wenzelm |
more systematic support for special directories;
|
file |
diff |
annotate
|
Fri, 17 Jul 2020 19:10:24 +0200 |
wenzelm |
clarified -- avoid non-standard extend/merge;
|
file |
diff |
annotate
|
Sat, 02 Nov 2019 12:02:27 +0100 |
wenzelm |
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
|
file |
diff |
annotate
|
Mon, 01 Apr 2019 21:51:46 +0200 |
wenzelm |
tuned signature -- more exports;
|
file |
diff |
annotate
|
Sat, 30 Mar 2019 20:54:47 +0100 |
wenzelm |
clarified signature: more explicit type Path.binding;
|
file |
diff |
annotate
|
Fri, 29 Mar 2019 13:42:17 +0100 |
wenzelm |
clarified 'file_prefix';
|
file |
diff |
annotate
|
Thu, 28 Mar 2019 21:24:55 +0100 |
wenzelm |
"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
|
file |
diff |
annotate
|
Thu, 28 Mar 2019 12:39:34 +0100 |
wenzelm |
proper local_theory command;
|
file |
diff |
annotate
|
Wed, 27 Mar 2019 23:55:39 +0100 |
wenzelm |
more exports: avoid clones in AFP;
|
file |
diff |
annotate
|
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
|