src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Mon Nov 22 15:03:37 2021 +0100
+++ b/src/Pure/PIDE/markup.scala	Mon Nov 22 16:49:58 2021 +0100
@@ -778,6 +778,8 @@
 {
   def is_empty: Boolean = name.isEmpty
 
+  def position_properties: Position.T = properties.filter(Markup.position_property)
+
   def markup(s: String): String =
     YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))