| Sun, 30 Mar 2025 13:50:06 +0200 |
haftmann |
tuned namespace organisation
|
file |
diff |
annotate
|
| Sun, 30 Mar 2025 11:21:34 +0200 |
haftmann |
proper markup for target language code
|
file |
diff |
annotate
|
| Sun, 01 Dec 2024 14:01:47 +0100 |
wenzelm |
clarified signature: more operations;
|
file |
diff |
annotate
|
| Wed, 11 Sep 2024 20:06:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 11 Sep 2024 20:05:09 +0200 |
wenzelm |
more robust: global ML name space for markup elements;
|
file |
diff |
annotate
|
| Wed, 11 Sep 2024 12:32:11 +0200 |
wenzelm |
clarified signature and modules;
|
file |
diff |
annotate
|
| Tue, 10 Sep 2024 20:36:01 +0200 |
wenzelm |
clarified signature: prefer explicit type Bytes.T;
|
file |
diff |
annotate
|
| Tue, 10 Sep 2024 20:06:51 +0200 |
wenzelm |
clarified signature, roughly following Isabelle/Scala;
|
file |
diff |
annotate
|
| Mon, 09 Sep 2024 22:59:51 +0200 |
wenzelm |
more scalable;
|
file |
diff |
annotate
|
| Mon, 09 Sep 2024 22:40:33 +0200 |
wenzelm |
eliminate print mode "code_presentation" thanks to value-oriented Pretty.T operations;
|
file |
diff |
annotate
|
| Mon, 09 Sep 2024 21:32:11 +0200 |
wenzelm |
clarified Pretty.markup_block: use value-oriented YXML.output_markup, with final re-interpretation via print_mode in output_tree;
|
file |
diff |
annotate
|
| Mon, 09 Sep 2024 11:12:13 +0200 |
wenzelm |
clarified signature: more explicit type "ops";
|
file |
diff |
annotate
|
| Fri, 24 Mar 2023 18:30:17 +0000 |
haftmann |
more uniform approach towards satisfied applications
|
file |
diff |
annotate
|
| Sun, 12 Feb 2023 06:45:59 +0000 |
haftmann |
somehow more clear terminology
|
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, 28 Mar 2022 12:54:09 +0000 |
haftmann |
modernized handling of variables
|
file |
diff |
annotate
|
| Sun, 27 Mar 2022 19:27:52 +0000 |
haftmann |
prefer build combinator
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 20:01:43 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 18:33:52 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
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
|
| Tue, 24 Apr 2018 14:17:58 +0000 |
haftmann |
proper datatype for 8-bit characters
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Thu, 04 Dec 2014 16:51:54 +0100 |
haftmann |
tuned module structure
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 22:02:49 +0100 |
wenzelm |
discontinued obsolete \<^sync> marker;
|
file |
diff |
annotate
|
| Thu, 01 May 2014 09:30:36 +0200 |
haftmann |
centralized upper/lowercase name mangling
|
file |
diff |
annotate
|
| Sat, 01 Feb 2014 18:42:46 +0100 |
wenzelm |
proper context for printing;
|
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 |
avoid (now superfluous) indirect passing of constant names
|
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
|
| Sun, 23 Jun 2013 21:16:06 +0200 |
haftmann |
tuned variable names
|
file |
diff |
annotate
|
| Fri, 24 May 2013 23:57:24 +0200 |
haftmann |
dedicated module for code symbol data
|
file |
diff |
annotate
|
| Fri, 24 May 2013 23:57:24 +0200 |
haftmann |
symbol data covers class relations also
|
file |
diff |
annotate
|
| Tue, 21 May 2013 12:03:05 +0200 |
wenzelm |
make SML/NJ happy;
|
file |
diff |
annotate
|
| Mon, 20 May 2013 13:29:45 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 19 May 2013 20:15:00 +0200 |
haftmann |
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
|
file |
diff |
annotate
|
| Sun, 19 May 2013 20:15:00 +0200 |
haftmann |
tuned and clarified
|
file |
diff |
annotate
|
| Sun, 19 May 2013 20:15:00 +0200 |
haftmann |
tuned, including signature
|
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
|
| Fri, 28 Dec 2012 09:37:27 +0100 |
haftmann |
formally corrected
|
file |
diff |
annotate
|
| Thu, 27 Dec 2012 21:01:08 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 27 Dec 2012 21:01:08 +0100 |
haftmann |
uniform parentheses for constructor -- necessary to accomodate scala 10
|
file |
diff |
annotate
|
| Thu, 27 Dec 2012 11:32:28 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Tue, 05 Jun 2012 07:05:56 +0200 |
haftmann |
prefer records with speaking labels over deeply nested tuples
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 10:16:51 +0200 |
haftmann |
dropped dead code;
|
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
|
| 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
|
| Sat, 23 Jul 2011 16:37:17 +0200 |
wenzelm |
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 17:51:49 +0200 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
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, 20 Nov 2010 00:53:26 +0100 |
wenzelm |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
file |
diff |
annotate
|
| Fri, 24 Sep 2010 14:03:44 +0200 |
haftmann |
always add trailing newline for presentation
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 13:23:21 +0200 |
haftmann |
reverted cs 07549694e2f1
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 11:29:22 +0200 |
haftmann |
shifted abstraction over imperative print mode
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 14:36:54 +0200 |
haftmann |
use buffers instead of string concatenation
|
file |
diff |
annotate
|