RFR: JDK-8307184: Incorrect/inconsistent specification and implementation for Elements.getDocComment [v5]

[Jonathan Gibbons]

On Sun, 6 Aug 2023 20:43:51 GMT, Joe Darcy <darcy at openjdk.org> wrote:

> > General feedback: while the text is good at describing when non-newline characters are removed, it is less good at describing the treatment of newlines ... are they line-terminators or line-separators; how do such characters in the result of `getDocComment` relate to the characters in the source file? For example, does `getDocComment` "copy" the newline characters found in the source file or are they always normalized to `\n` ?
> 
> Hmm. Does the precise handling of line terminators matter enough to specify?

Medium yes. For anyone parsing the contents of a doc comment, it helps to know whether the terminators are "as in the source file" or "always `\n`".   I guess if unspecified, users will have to assume the worst case (may be as in the source file) even if that is not typically the case.

-------------

PR Comment: https://git.openjdk.org/jdk/pull/15062#issuecomment-1671751731