author | wenzelm |
Thu, 25 Aug 2022 11:24:13 +0200 | |
changeset 75964 | fd9734380709 |
parent 75963 | 884dbbc8e1b3 |
child 75965 | fe686d96d7ff |
--- a/src/Pure/System/java.ML Wed Aug 24 08:22:13 2022 +0000 +++ b/src/Pure/System/java.ML Thu Aug 25 11:24:13 2022 +0200 @@ -26,7 +26,8 @@ | "\\" => "\\\\" | s => let val c = ord s in - if c < 16 then "\\u000" ^ Int.fmt StringCvt.HEX c + if 32 < c andalso c < 127 andalso c <> 34 andalso c <> 92 then s + else if c < 16 then "\\u000" ^ Int.fmt StringCvt.HEX c else if c < 128 then "\\u00" ^ Int.fmt StringCvt.HEX c else error ("Cannot print non-ASCII Java/Scala string literal: " ^ quote s) end;