# HG changeset patch
# User wenzelm
# Date 1674054941 -3600
# Node ID 19a7046f90f9e04f0a6f81fa8c387595ee53d8e9
# Parent  d9a4b3a73d8c7bea9ceb1ee9dbe45c8493e04da0
clarified signature;

diff -r d9a4b3a73d8c -r 19a7046f90f9 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Jan 18 16:04:51 2023 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Jan 18 16:15:41 2023 +0100
@@ -248,7 +248,7 @@
         (for {
           (command, line) <-
             Node.Commands.starts(commands.iterator, init = 1,
-              count = cmd => cmd.source.count(_ == '\n'))
+              count = cmd => Library.count_newlines(cmd.source))
         } yield command.id -> line).toMap
 
       lazy val load_commands: List[Command] =
@@ -706,7 +706,7 @@
         range = Text.Range(0, command.chunk.decode(offset))
         text <- range.try_substring(command.source)
         line <- node.command_start_line(command)
-      } yield line + text.count(_ == '\n')
+      } yield line + Library.count_newlines(text)
 
     def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] =
       if (other_node_name.is_theory) {
diff -r d9a4b3a73d8c -r 19a7046f90f9 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Wed Jan 18 16:04:51 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Wed Jan 18 16:15:41 2023 +0100
@@ -178,7 +178,7 @@
           }
           if (chunk.is_malformed && err_line == 0) { err_line = line }
           offset = end_offset
-          line += chunk.source.count(_ == '\n')
+          line += Library.count_newlines(chunk.source)
         }
 
         val err_pos =
diff -r d9a4b3a73d8c -r 19a7046f90f9 src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Wed Jan 18 16:04:51 2023 +0100
+++ b/src/Pure/Thy/latex.scala	Wed Jan 18 16:15:41 2023 +0100
@@ -275,7 +275,7 @@
       def traverse(xml: XML.Body): Unit = {
         xml.foreach {
           case XML.Text(s) =>
-            line += s.count(_ == '\n')
+            line += Library.count_newlines(s)
             result += s
           case elem @ XML.Elem(markup, body) =>
             val a = Markup.Optional_Argument.get(markup.properties)
diff -r d9a4b3a73d8c -r 19a7046f90f9 src/Pure/library.scala
--- 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")
diff -r d9a4b3a73d8c -r 19a7046f90f9 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Jan 18 16:04:51 2023 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Jan 18 16:15:41 2023 +0100
@@ -252,7 +252,7 @@
       val formatted = Pretty.formatted(info.info, margin = margin, metric = metric)
       val lines =
         XML.traverse_text(formatted)(if (XML.text_length(formatted) == 0) 0 else 1)(
-          (n: Int, s: String) => n + s.iterator.count(_ == '\n'))
+          (n: Int, s: String) => n + Library.count_newlines(s))
 
       val h = painter.getLineHeight * lines + geometry.deco_height
       val margin1 =