[isabelle] Isabelle2016-1-RC1: Printing of literal newline characters in Scala code is wrong
- To: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>
- Subject: [isabelle] Isabelle2016-1-RC1: Printing of literal newline characters in Scala code is wrong
- From: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
- Date: Tue, 1 Nov 2016 16:44:05 +0100
- In-reply-to: <firstname.lastname@example.org>
- References: <alpine.LNX.email@example.com> <firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0
Dear Isabelle developers,
The code generator seems to print literal strings (String.literal) differently in
Isabelle2016-1-RC1 than it did in Isabelle2016, at least for the target language Scala.
Here's a minimal example:
definition "newline = STR [Char Nibble0 NibbleB]" (* Isabelle2016 *)
definition "newline = STR ''â''" (* Isabelle2016-1-RC1 *)
export_code newline in Scala
In Isabelle2016, the newline constant is printed as
def newline: String = "\12"
in octal notation. 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.
In Haskell, OCaml, and SML, a newline gets pretty-printed as "\n". Why can't we just use
this also for Scala?
This archive was generated by a fusion of
Pipermail (Mailman edition) and