more accurate message boundaries;
authorwenzelm
Thu, 07 Nov 2024 20:43:25 +0100
changeset 81397 9f46260073c8
parent 81396 c3046c9b5fe9
child 81398 f92ea68473f2
more accurate message boundaries;
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)