explicit model concerning files of generated code

more correct error message

proper datatype for 8-bit characters

clarified position;

dedicated case option for code generation to Scala

--HG--
extra : rebase_source : f4d2da47982250c33b66f81d009da3f3d0b48bbd

corrected slip

--HG--
extra : rebase_source : 10ec2fab9a8984c22cdc48592342612979d6aa34

tuned

--HG--
extra : rebase_source : 5fe223879d21e15dec10febab3da774a4ccafa27

more uniform isabelle_scala;
more uniform ISABELLE_SCALAC_OPTIONS with heap options;

uniform use of ISABELLE_SCALAC_OPTIONS for scalac, notably for -Xmax-classfile-name on encrypted or docker file-systems;

Scala "\u" notation uses hexadecimal, not octal (amending 00a135c0a17f);

compiling implicit instances into companion objects for classes avoids ambiguities

--HG--
extra : rebase_source : 0754a0f98b2ef613dbdb8459c02a66aaa6418093

non-deprecated char literals for Scala

explicit resolution of ambiguous dictionaries

unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup

modernized and more uniform style

allow multiple inheritance of targets

--HG--
extra : rebase_source : 9d4980222d189226728427249e77a98373cb2011

accomplish potentially case-insenstive file systems for Scala

--HG--
extra : rebase_source : 01775a1b8de5b9b7744107f7a87f3c79d88af6d0

simplified and tuned using signed_string_of_int

--HG--
extra : rebase_source : 46a7964c9bf25560a84b216293068a268d5b6700

enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)

centralized upper/lowercase name mangling

--HG--
extra : rebase_source : 9afb0b542ffd66bd6bcf3a4990fe5063573500be

amended some slips, rolling back currently dysfunctional export minimimalisation for Scala

keep only identifiers public which are explicitly requested or demanded by dependencies

explicit option for "open" code generation

more fine-grain notion of export

formal markup for public ingredients

more suitable names, without any notion of "activating"

less clumsy namespace

prefer explicit code symbol type over ad-hoc name mangling

more abstract declaration of unqualified constant names in code printing context

consider explicit hint for domain of class parameters when printing instance statements

explicit hint for domain of class parameters in instance statements

migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

space between minus sign and number for large negative number literals causes NumberFormatException at run-time

bookkeeping and input syntax for exact specification of names of symbols in generated code

--HG--
extra : rebase_source : 60e91890f26f4c44ec2fa3a5be594fa7f2c1bdd0

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

uniform parentheses for constructor -- necessary to accomodate scala 10

evaluation: allow multiple code modules

prefer sys.error over plain error in Scala to avoid deprecation warning

prefer records with speaking labels over deeply nested tuples

--HG--
extra : rebase_source : 09acb7079a2d06a9c7f68aaaf04cedb0752142e0

dropped sort constraints on datatype specifications

dropped dead code

always bracket case expressions in Scala

syntactic improvements and tuning names in the code generator due to Florian's code review

adding the body type as well to the code generation for constants as it is required for type annotations of constants

changing const type to pass along if typing annotations are necessary for disambigous terms

refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;

tuned signature: Name.invent and Name.invent_names;

simplified Name.variant -- discontinued builtin fold_map;

allow spaces in executable names;
simplified generated bash scripts;

tuned;

dropped redundancy

more idiomatic printing of let cascades and type variable constraints

scala serializer adds parentheses around function literals

program is separate argument to serializer

scala is reserved identifier

printing combinator for hierarchical programs

dropped names from serializer interface

hand out deresolver from serializer invocation

restored and added surpression of case combinators

dropped superfluous presentation names

manage statement selection for presentation wholly through markup

formal markup of generated code for statements

formal framework for presentation of selected statements

include names need not be considered as reserved any longer

simultaneous modification of statements: statement names

simultaneous modification of statements

explicit modify_stmt parameter

factored out generic part of Scala serializer into code_namespace.ML

do not print object frame around Scala includes -- this is in the responsibility of the user

tuned internally and made smlnj happy

dropped single_module parameter

record argument for serializers

removed serializer interface redundancies

more coherent naming of syntax data structures

Code_Printer.tuplify

tuned

tuned

tuned

eliminated some obscure higher-order arguments

width is a formal parameter of serialization

code checking: compiler invocation happens in same directory as generated file -- avoid problem with different path representations on cygwin

improved deresolving of implicits

proper namespace administration for hierarchical modules

only print qualified implicits

stub for (later) correct deresolving of class method names

tuned serializer interface

private version of commas, cf. printmode

corrected semantics of presentation_stmt_names; do not print includes on presentation selection

code_include Scala: qualify module nmae

preliminary implementation of hierarchical module name space

tuned printing of applications and let cascades

another refinement chapter in the neverending numeral story

more generous memory settings for scala check

datatype classes are abstract

distinguish different classes of const syntax

use generic description slot for formal code checking

formal slot for code checker

check without explicit path

dropped ancient in-place compilation of SML

checking generated code for various target languages

once more a try with mkdir_leaf

revert to plain for now mkdir

mkdir_leaf -- avoiding surprises with typos in user-given paths

pervasive tuning of code

tuned whitespace; dropped dead code

dropped dead code

first serious draft of a scala code generator

transitive superclasses were also only a misunderstanding

formal introduction of transitive superclasses

dropped obscure type argument weakening mapping -- was only a misunderstanding

drop function definitions of combinators

formal introduction of case cong

more consistent naming aroud type classes and instances

avoid "$"

capitalized type variables; added yield as keyword

corrected printing of characters

more coherent naming with ML serializer

context theorem is optional

code literals: distinguish numeral classes by different entries

tuned for products vs. tupled functions

being more accurate wrt. list syntax

proper types for user-defined syntax

a primitive scala serializer