[m-rev.] diff: avoid \u in java comments

[Peter Wang]

Reported in bug #108.

Branches: main

compiler/mlds_to_java.m:
        Replace "\u" by "\\u" in context line comments, as the former will be
        treated as Unicode escapes.

diff --git a/compiler/mlds_to_java.m b/compiler/mlds_to_java.m
index 613e9b9..8229e62 100644
--- a/compiler/mlds_to_java.m
+++ b/compiler/mlds_to_java.m
@@ -4551,8 +4551,10 @@ output_context(Info, Context, !IO) :-
             File \= ""
         ->
             % Java doesn't have an equivalent of #line directives.
+            % \u is treated as a Unicode escape even with comments.
             io.write_string("// ", !IO),
-            io.write_string(File, !IO),
+            string.replace_all(File, "\\u", "\\\\u", SafePath),
+            io.write_string(SafePath, !IO),
             io.write_string(":", !IO),
             io.write_int(Line, !IO),
             io.nl(!IO),

--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to:       mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions:          mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------