Re: [isabelle] Isabelle2016-1-RC1: Printing of literal newline characters in Scala code is wrong
On 01/11/16 16:44, Andreas Lochbihler wrote:
> definition "newline = STR ''â''" (* Isabelle2016-1-RC1 *)
> export_code newline in Scala
> In Isabelle2016-1-RC1, it is printed as
> def newline: String = "\u0012"
> which uses hexadecimal notation, but the numbers are still the same, so
> this is actually the character at codepoint 18. The same problem occurs
> for other characters that are output in \uNNNN notation.
Interestingly, the deprecation of Scala's octal \NNN in favour of
hexadecimal \uNNNN was motivated by avoidance of such mistakes
concerning the base of numerals.
I have now changed that here
It shows that there can be errors in formally verified and generated
programs, but that should not be surprising to users who understand how
> In Haskell, OCaml, and SML, a newline gets pretty-printed as "\n". Why
> can't we just use this also for Scala?
That uniform, but awkward use of \u actually exposed the mistake in the
Florian Haftmann, who is presently on vacation, is free to refine that
further in post-release development.
This archive was generated by a fusion of
Pipermail (Mailman edition) and