more readable string literals;
authorwenzelm
Thu, 25 Aug 2022 11:24:13 +0200
changeset 75964 fd9734380709
parent 75963 884dbbc8e1b3
child 75965 fe686d96d7ff
more readable string literals;
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;