# HG changeset patch
# User wenzelm
# Date 1731008605 -3600
# Node ID 9f46260073c8392f63cf171f6c1249db9b873978
# Parent  c3046c9b5fe95314e53bd7075034be90c5de8066
more accurate message boundaries;

diff -r c3046c9b5fe9 -r 9f46260073c8 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Thu Nov 07 20:37:11 2024 +0100
+++ b/src/Pure/PIDE/rendering.scala	Thu Nov 07 20:43:25 2024 +0100
@@ -670,10 +670,10 @@
 
           case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
             val file = perhaps_append_file(snapshot.node_name, name)
-            val text =
-              if (name == file) "file " + quote(file)
-              else "path " + quote(name) + "\nfile " + quote(file)
-            Some(info.add_info_text(r0, text))
+            val info1 =
+              if (name == file) info
+              else info.add_info_text(r0, "path " + quote(name))
+            Some(info1.add_info_text(r0, "file " + quote(file)))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) =>
             val text = "doc " + quote(name)