[581345] DiagnosticDecorator.escapeContent(String) does not strip '003'

from the result
ewillink · Jan 13, 2023 · ad70aa0 · ad70aa0
1 parent 36cee1a
commit ad70aa0
Showing 1 changed file with 4 additions and 5 deletions.
diff --git a/...ins/org.eclipse.emf.edit.ui/src/org/eclipse/emf/edit/ui/provider/DiagnosticDecorator.java b/...ins/org.eclipse.emf.edit.ui/src/org/eclipse/emf/edit/ui/provider/DiagnosticDecorator.java
@@ -114,11 +114,6 @@ public static String escapeContent(String content)
             escape = false;
             break;
           }
-          case '\003':
-          {
-            escape = true;
-            break;
-          }
           case ' ':
           {
             result.append("&#160;");
@@ -141,6 +136,10 @@ public static String escapeContent(String content)
           }
         }
       }
+      else if (character == '\003')
+      {
+        escape = true;
+      }
       else
       {
         result.append(character);