[isabelle] Isabelle2016-1-RC1: Printing of literal newline characters in Scala code is wrong



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?

Andreas




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