--- a/src/Tools/Code/code_scala.ML Tue Jun 14 20:48:41 2016 +0200
+++ b/src/Tools/Code/code_scala.ML Tue Jun 14 20:48:42 2016 +0200
@@ -429,7 +429,8 @@
else if c = "\"" then "\\\""
else if c = "\\" then "\\\\"
else let val k = ord c
- in if k < 32 orelse k > 126 then "\\" ^ radixstring (8, "0", k) else c end
+ in if k < 32 orelse k > 126
+ then "\\u" ^ align_right "0" 4 (radixstring (8, "0", k)) else c end
fun numeral_scala k =
if ~2147483647 < k andalso k <= 2147483647
then signed_string_of_int k