--- a/src/Pure/PIDE/protocol.scala Wed Oct 29 14:48:25 2025 +0100
+++ b/src/Pure/PIDE/protocol.scala Wed Oct 29 15:03:59 2025 +0100
@@ -6,6 +6,9 @@
package isabelle
+import scala.collection.mutable
+import scala.annotation.tailrec
+
object Protocol {
/* markers for inlined messages */
@@ -251,14 +254,27 @@
/* sendback snippets */
- def senback_snippets(body: XML.Body): List[(String, Properties.T)] = {
- body match {
- case XML.Elem(Markup(Markup.SENDBACK, props), b) :: rest =>
- (XML.content(b), props) :: senback_snippets(rest)
- case XML.Elem(_, b) :: rest => senback_snippets(b ::: rest)
- case _ :: rest => senback_snippets(rest)
- case Nil => Nil
- }
+ def senback_snippets(xml: XML.Body): List[(String, Properties.T)] = {
+ var seen = Set.empty[(String, Properties.T)]
+ val result = new mutable.ListBuffer[(String, Properties.T)]
+
+ @tailrec def traverse(body: XML.Body): Unit =
+ body match {
+ case XML.Elem(Markup(Markup.SENDBACK, props), body1) :: body2 =>
+ val entry = (XML.content(body1), props)
+ if (!seen(entry)) {
+ seen += entry
+ result += entry
+ }
+ traverse(body2)
+ case XML.Wrapped_Elem(_, _, body1) :: body2 => traverse(body1 ::: body2)
+ case XML.Elem(_, body1) :: body2 => traverse(body1 ::: body2)
+ case XML.Text(_) :: body2 => traverse(body2)
+ case Nil =>
+ }
+
+ traverse(xml)
+ result.toList
}