src/Pure/General/bytes.scala

--- a/src/Pure/General/bytes.scala	Wed Jul 03 20:35:10 2024 +0200
+++ b/src/Pure/General/bytes.scala	Wed Jul 03 20:59:30 2024 +0200
@@ -374,6 +374,9 @@
     }
     else bytes
 
+  def terminated_line: Boolean =
+    size >= 1 && (byte_unchecked(size - 1) == 13 || byte_unchecked(size - 1) == 10)
+
   def trim_line: Bytes =
     if (size >= 2 && byte_unchecked(size - 2) == 13 && byte_unchecked(size - 1) == 10) {
       slice(0, size - 2)