make/jdk/src/classes/build/tools/fixuppandoc/Main.java
changeset 55651 45fc36beb0aa
parent 55300 1e0b948cc122
child 58679 9c3209ff7550
--- a/make/jdk/src/classes/build/tools/fixuppandoc/Main.java	Thu Jul 11 08:19:56 2019 +0900
+++ b/make/jdk/src/classes/build/tools/fixuppandoc/Main.java	Wed Jul 10 16:23:59 2019 -0700
@@ -81,6 +81,10 @@
  *
  * Update the content string, to indicate it has been processed by this program.
  *
+ * <h2>{@code <nav id="TOC">}</h2>
+ *
+ * Set attribute {@code title="Table Of Contents"}
+ *
  */
 public class Main {
     /**
@@ -273,6 +277,11 @@
                     }
                     // <main> is not permitted within these elements
                     allowMain = false;
+                    if (name.equals("nav") && Objects.equals(attrs.get("id"), "TOC")) {
+                        out.write(buffer.toString()
+                                .replaceAll(">$", " title=\"Table Of Contents\">"));
+                        buffer.setLength(0);
+                    }
                     break;
 
                 case "body":