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

[Jonathan Gibbons]

On Wed, 9 Aug 2023 16:24:57 GMT, Jonathan Gibbons <jjg 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.

I guess for anyone doing character-based parsing, handling line-ending sequences is no biggie.  For folk doing line-based parsing `String.lines()` comes to mind ...

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

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