diff -r f1380c9f3806 -r 0cc96d337e8f src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Wed Nov 25 15:12:02 2020 +0100
+++ b/src/Pure/General/position.scala	Wed Nov 25 15:24:55 2020 +0100
@@ -112,14 +112,12 @@
       }
   }
 
-  def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
-
 
   /* here: user output */
 
   def here(props: T, delimited: Boolean = true): String =
   {
-    val pos = props.filter(p => Markup.POSITION_PROPERTIES(p._1))
+    val pos = props.filter(Markup.position_property)
     if (pos.isEmpty) ""
     else {
       val s0 =