#
28b11dd3 |
|
09-Jan-2019 |
haftmann <none@none> |
explicit model concerning files of generated code
|
#
f70035d2 |
|
25-Apr-2018 |
haftmann <none@none> |
more correct error message
|
#
3a4a7136 |
|
24-Apr-2018 |
haftmann <none@none> |
proper datatype for 8-bit characters
|
#
ee98c305 |
|
24-Jan-2018 |
wenzelm <none@none> |
clarified position;
|
#
515bdf02 |
|
14-Dec-2017 |
haftmann <none@none> |
dedicated case option for code generation to Scala --HG-- extra : rebase_source : f4d2da47982250c33b66f81d009da3f3d0b48bbd
|
#
08a997a6 |
|
02-Aug-2017 |
haftmann <none@none> |
corrected slip --HG-- extra : rebase_source : 10ec2fab9a8984c22cdc48592342612979d6aa34
|
#
430c70a9 |
|
02-Aug-2017 |
haftmann <none@none> |
tuned --HG-- extra : rebase_source : 5fe223879d21e15dec10febab3da774a4ccafa27
|
#
44e91cea |
|
21-Apr-2017 |
wenzelm <none@none> |
more uniform isabelle_scala; more uniform ISABELLE_SCALAC_OPTIONS with heap options;
|
#
37cb5ea9 |
|
15-Jan-2017 |
wenzelm <none@none> |
uniform use of ISABELLE_SCALAC_OPTIONS for scalac, notably for -Xmax-classfile-name on encrypted or docker file-systems;
|
#
883d7651 |
|
05-Nov-2016 |
wenzelm <none@none> |
Scala "\u" notation uses hexadecimal, not octal (amending 00a135c0a17f);
|
#
537211d8 |
|
23-Jun-2016 |
haftmann <none@none> |
compiling implicit instances into companion objects for classes avoids ambiguities --HG-- extra : rebase_source : 0754a0f98b2ef613dbdb8459c02a66aaa6418093
|
#
b76ea1d3 |
|
14-Jun-2016 |
haftmann <none@none> |
non-deprecated char literals for Scala
|
#
1a3088a0 |
|
14-Jun-2016 |
haftmann <none@none> |
explicit resolution of ambiguous dictionaries
|
#
db9f4005 |
|
06-Sep-2015 |
haftmann <none@none> |
unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup
|
#
0285f5b6 |
|
09-Jan-2015 |
haftmann <none@none> |
modernized and more uniform style
|
#
0976a200 |
|
05-Dec-2014 |
haftmann <none@none> |
allow multiple inheritance of targets --HG-- extra : rebase_source : 9d4980222d189226728427249e77a98373cb2011
|
#
31e1aaa1 |
|
02-Oct-2014 |
haftmann <none@none> |
accomplish potentially case-insenstive file systems for Scala --HG-- extra : rebase_source : 01775a1b8de5b9b7744107f7a87f3c79d88af6d0
|
#
b12d2aca |
|
18-Sep-2014 |
haftmann <none@none> |
simplified and tuned using signed_string_of_int --HG-- extra : rebase_source : 46a7964c9bf25560a84b216293068a268d5b6700
|
#
b7f1a757 |
|
02-May-2014 |
haftmann <none@none> |
enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)
|
#
5607f158 |
|
01-May-2014 |
haftmann <none@none> |
centralized upper/lowercase name mangling --HG-- extra : rebase_source : 9afb0b542ffd66bd6bcf3a4990fe5063573500be
|
#
32a521c9 |
|
27-Feb-2014 |
haftmann <none@none> |
amended some slips, rolling back currently dysfunctional export minimimalisation for Scala
|
#
217fdae1 |
|
23-Feb-2014 |
haftmann <none@none> |
keep only identifiers public which are explicitly requested or demanded by dependencies
|
#
34a077b1 |
|
23-Feb-2014 |
haftmann <none@none> |
explicit option for "open" code generation
|
#
950cc03c |
|
23-Feb-2014 |
haftmann <none@none> |
more fine-grain notion of export
|
#
8b24d313 |
|
23-Feb-2014 |
haftmann <none@none> |
formal markup for public ingredients
|
#
463293a2 |
|
26-Jan-2014 |
haftmann <none@none> |
more suitable names, without any notion of "activating"
|
#
07ad0bb4 |
|
25-Jan-2014 |
haftmann <none@none> |
less clumsy namespace
|
#
9250249f |
|
25-Jan-2014 |
haftmann <none@none> |
prefer explicit code symbol type over ad-hoc name mangling
|
#
85e946f2 |
|
25-Jan-2014 |
haftmann <none@none> |
more abstract declaration of unqualified constant names in code printing context
|
#
6b292362 |
|
04-Jul-2013 |
haftmann <none@none> |
consider explicit hint for domain of class parameters when printing instance statements
|
#
3e492425 |
|
04-Jul-2013 |
haftmann <none@none> |
explicit hint for domain of class parameters in instance statements
|
#
a7b3de52 |
|
23-Jun-2013 |
haftmann <none@none> |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier --HG-- extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b
|
#
6b3992ad |
|
30-May-2013 |
Andreas Lochbihler <none@none> |
space between minus sign and number for large negative number literals causes NumberFormatException at run-time
|
#
8efa9794 |
|
24-May-2013 |
haftmann <none@none> |
bookkeeping and input syntax for exact specification of names of symbols in generated code --HG-- extra : rebase_source : 60e91890f26f4c44ec2fa3a5be594fa7f2c1bdd0
|
#
5a8927d0 |
|
15-Feb-2013 |
haftmann <none@none> |
two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one --HG-- extra : rebase_source : ffa0242ad108fe680ff144a716257c0784285d17
|
#
b844c4d1 |
|
27-Dec-2012 |
haftmann <none@none> |
uniform parentheses for constructor -- necessary to accomodate scala 10
|
#
c3e8fd6a |
|
27-Jul-2012 |
haftmann <none@none> |
evaluation: allow multiple code modules
|
#
408255f2 |
|
04-Jun-2012 |
haftmann <none@none> |
prefer sys.error over plain error in Scala to avoid deprecation warning
|
#
dc977d45 |
|
04-Jun-2012 |
haftmann <none@none> |
prefer records with speaking labels over deeply nested tuples --HG-- extra : rebase_source : 09acb7079a2d06a9c7f68aaaf04cedb0752142e0
|
#
8ceda7e9 |
|
28-May-2012 |
haftmann <none@none> |
dropped sort constraints on datatype specifications
|
#
070c6dd5 |
|
19-Apr-2012 |
haftmann <none@none> |
dropped dead code
|
#
dd64061c |
|
09-Mar-2012 |
haftmann <none@none> |
always bracket case expressions in Scala
|
#
5a712294 |
|
20-Sep-2011 |
bulwahn <none@none> |
syntactic improvements and tuning names in the code generator due to Florian's code review
|
#
20767fdb |
|
07-Sep-2011 |
bulwahn <none@none> |
adding the body type as well to the code generation for constants as it is required for type annotations of constants
|
#
0b9a2ceb |
|
07-Sep-2011 |
bulwahn <none@none> |
changing const type to pass along if typing annotations are necessary for disambigous terms
|
#
d049bd7b |
|
20-Aug-2011 |
wenzelm <none@none> |
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
|
#
b6f9ad57 |
|
09-Jun-2011 |
wenzelm <none@none> |
tuned signature: Name.invent and Name.invent_names;
|
#
1a5a42ee |
|
09-Jun-2011 |
wenzelm <none@none> |
simplified Name.variant -- discontinued builtin fold_map;
|
#
9ad65a83 |
|
13-Mar-2011 |
wenzelm <none@none> |
allow spaces in executable names; simplified generated bash scripts;
|
#
1e0ee16a |
|
13-Mar-2011 |
wenzelm <none@none> |
tuned;
|
#
7852386a |
|
19-Feb-2011 |
haftmann <none@none> |
dropped redundancy
|
#
e0f3edf5 |
|
17-Feb-2011 |
haftmann <none@none> |
more idiomatic printing of let cascades and type variable constraints
|
#
e4f97ce4 |
|
02-Feb-2011 |
bulwahn <none@none> |
scala serializer adds parentheses around function literals
|
#
98274748 |
|
21-Dec-2010 |
haftmann <none@none> |
program is separate argument to serializer
|
#
463bf26e |
|
29-Sep-2010 |
haftmann <none@none> |
scala is reserved identifier
|
#
dfb16b2f |
|
04-Sep-2010 |
haftmann <none@none> |
printing combinator for hierarchical programs
|
#
e0e92b2c |
|
04-Sep-2010 |
haftmann <none@none> |
dropped names from serializer interface
|
#
6d96da30 |
|
02-Sep-2010 |
haftmann <none@none> |
hand out deresolver from serializer invocation
|
#
fef022c6 |
|
02-Sep-2010 |
haftmann <none@none> |
restored and added surpression of case combinators
|
#
29dcd16b |
|
02-Sep-2010 |
haftmann <none@none> |
dropped superfluous presentation names
|
#
c63f8622 |
|
02-Sep-2010 |
haftmann <none@none> |
manage statement selection for presentation wholly through markup
|
#
760b2c60 |
|
02-Sep-2010 |
haftmann <none@none> |
formal markup of generated code for statements
|
#
6d9e22df |
|
01-Sep-2010 |
haftmann <none@none> |
formal framework for presentation of selected statements
|
#
5874e157 |
|
02-Sep-2010 |
haftmann <none@none> |
include names need not be considered as reserved any longer
|
#
9f818b6b |
|
01-Sep-2010 |
haftmann <none@none> |
simultaneous modification of statements: statement names
|
#
d766e612 |
|
01-Sep-2010 |
haftmann <none@none> |
simultaneous modification of statements
|
#
819fc7df |
|
01-Sep-2010 |
haftmann <none@none> |
explicit modify_stmt parameter
|
#
fcadcf9f |
|
31-Aug-2010 |
haftmann <none@none> |
factored out generic part of Scala serializer into code_namespace.ML
|
#
aeafbbda |
|
01-Sep-2010 |
haftmann <none@none> |
do not print object frame around Scala includes -- this is in the responsibility of the user
|
#
94cad23a |
|
01-Sep-2010 |
haftmann <none@none> |
tuned internally and made smlnj happy
|
#
13daea3e |
|
31-Aug-2010 |
haftmann <none@none> |
dropped single_module parameter
|
#
c2bf7b3b |
|
31-Aug-2010 |
haftmann <none@none> |
record argument for serializers
|
#
df6809b2 |
|
31-Aug-2010 |
haftmann <none@none> |
removed serializer interface redundancies
|
#
7a8d28bc |
|
31-Aug-2010 |
haftmann <none@none> |
more coherent naming of syntax data structures
|
#
badd5aa1 |
|
31-Aug-2010 |
haftmann <none@none> |
Code_Printer.tuplify
|
#
0017b558 |
|
30-Aug-2010 |
haftmann <none@none> |
tuned
|
#
82283147 |
|
30-Aug-2010 |
haftmann <none@none> |
tuned
|
#
7faeece9 |
|
30-Aug-2010 |
haftmann <none@none> |
tuned
|
#
fa897977 |
|
30-Aug-2010 |
haftmann <none@none> |
eliminated some obscure higher-order arguments
|
#
8ee2a45e |
|
30-Aug-2010 |
haftmann <none@none> |
width is a formal parameter of serialization
|
#
93bcf928 |
|
30-Aug-2010 |
haftmann <none@none> |
code checking: compiler invocation happens in same directory as generated file -- avoid problem with different path representations on cygwin
|
#
57ac99f6 |
|
27-Aug-2010 |
haftmann <none@none> |
improved deresolving of implicits
|
#
e7e6bf13 |
|
27-Aug-2010 |
haftmann <none@none> |
proper namespace administration for hierarchical modules
|
#
e8dd3d14 |
|
26-Aug-2010 |
haftmann <none@none> |
only print qualified implicits
|
#
8ae24a61 |
|
26-Aug-2010 |
haftmann <none@none> |
stub for (later) correct deresolving of class method names
|
#
6ab291e0 |
|
26-Aug-2010 |
haftmann <none@none> |
tuned serializer interface
|
#
166cb6bc |
|
25-Aug-2010 |
haftmann <none@none> |
private version of commas, cf. printmode
|
#
a3cda29b |
|
26-Aug-2010 |
haftmann <none@none> |
corrected semantics of presentation_stmt_names; do not print includes on presentation selection
|
#
7d6e35a6 |
|
26-Aug-2010 |
haftmann <none@none> |
code_include Scala: qualify module nmae
|
#
5dfd9395 |
|
25-Aug-2010 |
haftmann <none@none> |
preliminary implementation of hierarchical module name space
|
#
252752da |
|
29-Jul-2010 |
haftmann <none@none> |
tuned printing of applications and let cascades
|
#
1ad44b2b |
|
24-Jul-2010 |
haftmann <none@none> |
another refinement chapter in the neverending numeral story
|
#
ff5bcfcb |
|
21-Jul-2010 |
haftmann <none@none> |
more generous memory settings for scala check
|
#
6904baf2 |
|
20-Jul-2010 |
haftmann <none@none> |
datatype classes are abstract
|
#
ede59fb5 |
|
19-Jul-2010 |
haftmann <none@none> |
distinguish different classes of const syntax
|
#
6728ff4f |
|
14-Jul-2010 |
haftmann <none@none> |
use generic description slot for formal code checking
|
#
c54f63c8 |
|
14-Jul-2010 |
haftmann <none@none> |
formal slot for code checker
|
#
134c2b0f |
|
14-Jul-2010 |
haftmann <none@none> |
check without explicit path
|
#
b5520044 |
|
08-Jul-2010 |
haftmann <none@none> |
dropped ancient in-place compilation of SML
|
#
515be4d6 |
|
08-Jul-2010 |
haftmann <none@none> |
checking generated code for various target languages
|
#
ae53558f |
|
01-Jul-2010 |
haftmann <none@none> |
once more a try with mkdir_leaf
|
#
16acb0c8 |
|
01-Jul-2010 |
haftmann <none@none> |
revert to plain for now mkdir
|
#
4dd3f473 |
|
29-Jun-2010 |
haftmann <none@none> |
mkdir_leaf -- avoiding surprises with typos in user-given paths
|
#
7eea1f09 |
|
30-Jun-2010 |
haftmann <none@none> |
pervasive tuning of code
|
#
7125ae23 |
|
18-Jun-2010 |
haftmann <none@none> |
tuned whitespace; dropped dead code
|
#
0e6261bc |
|
18-Jun-2010 |
haftmann <none@none> |
dropped dead code
|
#
fcee9e9a |
|
17-Jun-2010 |
haftmann <none@none> |
first serious draft of a scala code generator
|
#
3032d8aa |
|
17-Jun-2010 |
haftmann <none@none> |
transitive superclasses were also only a misunderstanding
|
#
233f64f3 |
|
17-Jun-2010 |
haftmann <none@none> |
formal introduction of transitive superclasses
|
#
7f4e9daa |
|
17-Jun-2010 |
haftmann <none@none> |
dropped obscure type argument weakening mapping -- was only a misunderstanding
|
#
d7eae967 |
|
15-Jun-2010 |
haftmann <none@none> |
drop function definitions of combinators
|
#
93fbbd8f |
|
15-Jun-2010 |
haftmann <none@none> |
formal introduction of case cong
|
#
5c97a57f |
|
07-Jun-2010 |
haftmann <none@none> |
more consistent naming aroud type classes and instances
|
#
d43372e9 |
|
04-Jun-2010 |
haftmann <none@none> |
avoid "$"
|
#
7e405116 |
|
01-Jun-2010 |
haftmann <none@none> |
capitalized type variables; added yield as keyword
|
#
2db7530a |
|
01-Jun-2010 |
haftmann <none@none> |
corrected printing of characters
|
#
4ee8ba5e |
|
29-Apr-2010 |
haftmann <none@none> |
more coherent naming with ML serializer
|
#
3161d8fa |
|
19-Feb-2010 |
haftmann <none@none> |
context theorem is optional
|
#
a22630a8 |
|
22-Jan-2010 |
haftmann <none@none> |
code literals: distinguish numeral classes by different entries
|
#
456c018a |
|
14-Jan-2010 |
haftmann <none@none> |
tuned for products vs. tupled functions
|
#
beb7ae79 |
|
13-Jan-2010 |
haftmann <none@none> |
being more accurate wrt. list syntax
|
#
c79e67b5 |
|
08-Jan-2010 |
haftmann <none@none> |
proper types for user-defined syntax
|
#
a9b59024 |
|
07-Jan-2010 |
haftmann <none@none> |
a primitive scala serializer
|