src/Pure/library.scala
changeset 77007 19a7046f90f9
parent 76788 ce44e714d573
child 77367 d27d1224c67f
--- a/src/Pure/library.scala	Wed Jan 18 16:04:51 2023 +0100
+++ b/src/Pure/library.scala	Wed Jan 18 16:15:41 2023 +0100
@@ -94,6 +94,8 @@
 
   /* lines */
 
+  def count_newlines(str: String): Int = str.count(_ == '\n')
+
   def terminate_lines(lines: IterableOnce[String]): String = {
     val it = lines.iterator
     if (it.isEmpty) "" else it.mkString("", "\n", "\n")