# HG changeset patch
# User bpatel
# Date 1374274979 25200
#      Fri Jul 19 16:02:59 2013 -0700
# Node ID 843659ece699889459239c6470e67265de2b3f73
# Parent  9083313d5733ca9be66bc52cf64b9b5d4dd2e39a
8016675: Make Javadoc pages more robust
Reviewed-by: jlaskey, ksrini

diff -r 9083313d5733 -r 843659ece699 src/share/classes/com/sun/tools/doclets/formats/html/markup/HtmlWriter.java
--- openjdk/langtools/src/share/classes/com/sun/tools/doclets/formats/html/markup/HtmlWriter.java	Fri Oct 25 16:10:09 2013 +0100
+++ openjdk/langtools/src/share/classes/com/sun/tools/doclets/formats/html/markup/HtmlWriter.java	Fri Jul 19 16:02:59 2013 -0700
@@ -289,7 +289,7 @@
             script.addAttr(HtmlAttr.TYPE, "text/javascript");
             String scriptCode = "<!--" + DocletConstants.NL +
                     "    if (location.href.indexOf('is-external=true') == -1) {" + DocletConstants.NL +
-                    "        parent.document.title=\"" + winTitle + "\";" + DocletConstants.NL +
+                    "        parent.document.title=\"" + escapeJavaScriptChars(winTitle) + "\";" + DocletConstants.NL +
                     "    }" + DocletConstants.NL +
                     "//-->" + DocletConstants.NL;
             RawHtml scriptContent = new RawHtml(scriptCode);
@@ -299,6 +299,53 @@
     }
 
     /**
+     * Returns a String with escaped special JavaScript characters.
+     *
+     * @param s String that needs to be escaped
+     * @return a valid escaped JavaScript string
+     */
+    private static String escapeJavaScriptChars(String s) {
+        StringBuilder sb = new StringBuilder();
+        for (int i = 0; i < s.length(); i++) {
+            char ch = s.charAt(i);
+            switch (ch) {
+                case '\b':
+                    sb.append("\\b");
+                    break;
+                case '\t':
+                    sb.append("\\t");
+                    break;
+                case '\n':
+                    sb.append("\\n");
+                    break;
+                case '\f':
+                    sb.append("\\f");
+                    break;
+                case '\r':
+                    sb.append("\\r");
+                    break;
+                case '"':
+                    sb.append("\\\"");
+                    break;
+                case '\'':
+                    sb.append("\\\'");
+                    break;
+                case '\\':
+                    sb.append("\\\\");
+                    break;
+                default:
+                    if (ch < 32 || ch >= 127) {
+                        sb.append(String.format("\\u%04X", (int)ch));
+                    } else {
+                        sb.append(ch);
+                    }
+                    break;
+            }
+        }
+        return sb.toString();
+    }
+
+    /**
      * Returns a content tree for the SCRIPT tag for the main page(index.html).
      *
      * @return a content for the SCRIPT tag
