# 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)