src/Pure/System/java.ML

--- 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;