tuned signature;

--- 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 =

--- a/src/Pure/PIDE/command.scala	Wed Nov 25 15:12:02 2020 +0100
+++ b/src/Pure/PIDE/command.scala	Wed Nov 25 15:24:55 2020 +0100
@@ -364,7 +364,7 @@
                         case (Some((target_name, target_chunk)), Position.Range(symbol_range)) =>
                           target_chunk.incorporate(symbol_range) match {
                             case Some(range) =>
-                              val props = Position.purge(atts)
+                              val props = atts.filterNot(Markup.position_property)
                               val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
                               state.add_markup(false, target_name, Text.Info(range, elem))
                             case None => bad(); state

--- a/src/Pure/PIDE/markup.ML	Wed Nov 25 15:12:02 2020 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Nov 25 15:24:55 2020 +0100
@@ -60,6 +60,7 @@
   val fileN: string
   val idN: string
   val position_properties: string list
+  val position_property: Properties.entry -> bool
   val positionN: string val position: T
   val expressionN: string val expression: string -> T
   val citationN: string val citation: string -> T
@@ -380,6 +381,7 @@
 val idN = "id";
 
 val position_properties = [lineN, offsetN, end_offsetN, fileN, idN];
+fun position_property (entry: Properties.entry) = member (op =) position_properties (#1 entry);
 
 val (positionN, position) = markup_elem "position";
 

--- a/src/Pure/PIDE/markup.scala	Wed Nov 25 15:12:02 2020 +0100
+++ b/src/Pure/PIDE/markup.scala	Wed Nov 25 15:24:55 2020 +0100
@@ -144,6 +144,8 @@
   val DEF_ID = "def_id"
 
   val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
+  def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1)
+
   val POSITION = "position"
 
 

--- a/src/Pure/Thy/export_theory.scala	Wed Nov 25 15:12:02 2020 +0100
+++ b/src/Pure/Thy/export_theory.scala	Wed Nov 25 15:24:55 2020 +0100
@@ -192,7 +192,7 @@
       case XML.Elem(Markup(Markup.ENTITY, props), body) =>
         val name = Markup.Name.unapply(props) getOrElse err()
         val xname = Markup.XName.unapply(props) getOrElse err()
-        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) && a != Markup.ID })
+        val pos = props.filter(p => Markup.position_property(p) && p._1 != Markup.ID)
         val id = Position.Id.unapply(props)
         val serial = Markup.Serial.unapply(props) getOrElse err()
         (Entity(kind, name, xname, pos, id, serial), body)