Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...);
authorwenzelm
Fri, 05 Apr 2024 20:41:54 +0200
changeset 80087 bda75c790bfa
parent 80086 1b986e5f9764
child 80088 5afbf04418ec
proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...);
src/HOL/String.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/String.thy	Fri Apr 05 17:47:09 2024 +0200
+++ b/src/HOL/String.thy	Fri Apr 05 20:41:54 2024 +0200
@@ -803,7 +803,7 @@
     (SML) "Str'_Literal.literal'_of'_asciis"
     and (OCaml) "Str'_Literal.literal'_of'_asciis"
     and (Haskell) "map/ (let chr k | (0 <= k && k < 128) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
-    and (Scala) "\"\"/ ++/ _.map((k: BigInt) => if (BigInt(0) <= k && k < BigInt(128)) k.charValue else sys.error(\"Non-ASCII character in literal\"))"
+    and (Scala) "_.map((k: BigInt) => if (BigInt(0) <= k && k < BigInt(128)) k.charValue else sys.error(\"Non-ASCII character in literal\")).mkString"
 | constant String.asciis_of_literal \<rightharpoonup>
     (SML) "Str'_Literal.asciis'_of'_literal"
     and (OCaml) "Str'_Literal.asciis'_of'_literal"
isabelle