(str) improve specification of String::lines

Summary

The specification for the String::lines method, introduced by JDK-8200380 (CSR: JDK-8200425) can be improved.

Problem

Certain definitions used in this specification, in particular the definition of "line," could be improved. It is important to get the definitions very precise since future APIs will depend on this same definitions.

Solution

Change the wording of the specifications to give more precise definitions. This is strictly an editorial spec change. No semantic change to the specification is intended, nor should any implementation change be necessary.

Specification

The revised specification for String::lines is as follows:

/**
 * Returns a stream of lines extracted from this string,
 * separated by line terminators.
 * <p>
 * A <i>line terminator</i> is one of the following:
 * a line feed character {@code "\n"} (U+000A),
 * a carriage return character {@code "\r"} (U+000D),
 * or a carriage return followed immediately by a line feed
 * {@code "\r\n"} (U+000D U+000A).
 * <p>
 * A <i>line</i> is either a sequence of zero or more characters
 * followed by a line terminator, or it is a sequence of one or
 * more characters followed by the end of the string. A
 * line does not include the line terminator.
 * <p>
 * The stream returned by this method contains the lines from
 * this string in the order in which they occur.
 *
 * @apiNote This definition of <i>line</i> implies that an empty
 *          string has zero lines and that there is no empty line
 *          following a line terminator at the end of a string.
 *
 * @implNote This method provides better performance than
 *           split("\R") by supplying elements lazily and
 *           by faster search of new line terminators.
 *
 * @return  the stream of lines extracted from this string
 *
 * @since 11
 */

Differences from the previous version of the specification, introduced earlier in JDK 11, are as follows:

 /**
- * Returns a stream of substrings extracted from this string
- * partitioned by line terminators.
+ * Returns a stream of lines extracted from this string,
+ * separated by line terminators.
  * <p>
- * Line terminators recognized are line feed
- * {@code "\n"} ({@code U+000A}),
- * carriage return
- * {@code "\r"} ({@code U+000D})
- * and a carriage return followed immediately by a line feed
- * {@code "\r\n"} ({@code U+000D U+000A}).
+ * A <i>line terminator</i> is one of the following:
+ * a line feed character {@code "\n"} (U+000A),
+ * a carriage return character {@code "\r"} (U+000D),
+ * or a carriage return followed immediately by a line feed
+ * {@code "\r\n"} (U+000D U+000A).
  * <p>
- * The stream returned by this method contains each line of
- * this string that is terminated by a line terminator except that
- * the last line can either be terminated by a line terminator or the
- * end of the string.
- * The lines in the stream are in the order in which
- * they occur in this string and do not include the line terminators
- * partitioning the lines.
+ * A <i>line</i> is either a sequence of zero or more characters
+ * followed by a line terminator, or it is a sequence of one or
+ * more characters followed by the end of the string. A
+ * line does not include the line terminator.
+ * <p>
+ * The stream returned by this method contains the lines from
+ * this string in the order in which they occur.
+ *
+ * @apiNote This definition of <i>line</i> implies that an empty
+ * string has zero lines and that there is no empty line
+ * following a line terminator at the end of a string.
  *
  * @implNote This method provides better performance than
  * split("\R") by supplying elements lazily and
  * by faster search of new line terminators.
  *
- * @return the stream of strings extracted from this string
- * partitioned by line terminators
+ * @return the stream of lines extracted from this string
  *
  * @since 11
  */