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
https://bitbucket.org/isabelle_project/isabelle-release/commits/bed02fca80b

It shows that there can be errors in formally verified and generated
programs, but that should not be surprising to users who understand how
things work.


> 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
first place.

Florian Haftmann, who is presently on vacation, is free to refine that
further in post-release development.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.