[isabelle-dev] scala-2.12.2

[Lars Hupel]

> I took the opportunity to have a look at it and found out it can be done
> differently, see attached patch.

The patch is now running on testboard:
<https://ci.isabelle.systems/jenkins/job/testboard/385/>.

> The clue about "integer_of_char" is that it had to work regardless
> whether HOL chars are represented authentic or by target language
> characters (importing "~~/src/HOL/Library/Code_Char").
> 
> Nowadays this can be achieved without spelling out the chars explicitly.
>  The last stone to turn around before had been the de-constructivation
> of the char type (b3f2b8c906a6).

Thanks for investigating this.

Cheers
Lars