# HG changeset patch
# User wenzelm
# Date 1658406577 -7200
# Node ID 49444d7f8337f20f1ae27d5ec42aee41e8862f58
# Parent  7ca63aea3c6c21b992fe0b60a81668154a172c53
tuned messages;

diff -r 7ca63aea3c6c -r 49444d7f8337 src/Pure/System/java.ML
--- a/src/Pure/System/java.ML	Thu Jul 21 14:27:11 2022 +0200
+++ b/src/Pure/System/java.ML	Thu Jul 21 14:29:37 2022 +0200
@@ -28,14 +28,14 @@
       let val c = ord s in
         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 Scala string literal: " ^ quote s)
+        else error ("Cannot print non-ASCII Java/Scala string literal: " ^ quote s)
       end;
 
 in
 
 fun print_string str =
   quote (translate_string print_str str)
-    handle Fail _ => error ("Cannot print non-ASCII Scala string literal: " ^ quote str);
+    handle Fail _ => error ("Cannot print non-ASCII Java/Scala string literal: " ^ quote str);
 
 end;