--- a/src/Pure/PIDE/protocol.scala Wed Oct 29 14:08:10 2025 +0100
+++ b/src/Pure/PIDE/protocol.scala Wed Oct 29 14:48:25 2025 +0100
@@ -249,6 +249,19 @@
}
+ /* 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
+ }
+ }
+
+
/* breakpoints */
object ML_Breakpoint {