--- 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) {
--- 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 =
--- 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)
--- 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")
--- 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 =