6558804: Specification for Elements.getDocComment(Element e) should be clarified

Reviewed-by: jjg

src/share/classes/javax/lang/model/util/Elements.java

@@ -77,9 +77,25 @@ public interface Elements {
      * Returns the text of the documentation ("Javadoc")
      * comment of an element.
      *
+     * <p> A documentation comment of an element is a comment that
+     * begins with "{@code /**}" , ends with a separate
+     * "<code>*&#47</code>", and immediately precedes the element,
+     * ignoring white space.  Therefore, a documentation comment
+     * contains at least three"{@code *}" characters.  The text
+     * returned for the documentation comment is a processed form of
+     * the comment as it appears in source code.  The leading "{@code
+     * /**}" and trailing "<code>*&#47</code>" are removed.  For lines
+     * of the comment starting after the initial "{@code /**}",
+     * leading white space characters are discarded as are any
+     * consecutive "{@code *}" characters appearing after the white
+     * space or starting the line.  The processed lines are then
+     * concatenated together (including line terminators) and
+     * returned.
+     *
      * @param e  the element being examined
      * @return the documentation comment of the element, or {@code null}
      *          if there is none
+     * @jls3 3.6 White Space
      */
     String getDocComment(Element e);