documentLines function
src split into lines: line endings normalised, and the empty line after
a final line ending dropped — it is the end of the last line, not a line.
Implementation
List<String> documentLines(String src) {
// Two full rewrites of the source, for a character most sources do not
// contain. Checking first is one scan that usually ends in none.
var normalized = src.contains('\r')
? src.replaceAll('\r\n', '\n').replaceAll('\r', '\n')
: src;
// CommonMark: U+0000 is replaced, for safety.
if (normalized.contains('\u0000')) {
normalized = normalized.replaceAll('\u0000', '�');
}
final lines = normalized.split('\n');
if (lines.length > 1 && lines.last.isEmpty) {
lines.removeLast();
}
return lines;
}