diff -r 0d8b5612a0a6 -r 135787601438 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Sat Nov 06 10:39:47 2021 +0100
+++ b/src/Pure/General/position.scala	Sat Nov 06 11:25:03 2021 +0100
@@ -63,6 +63,17 @@
       }
   }
 
+  object Def_Range
+  {
+    def apply(range: Symbol.Range): T = Def_Offset(range.start) ::: Def_End_Offset(range.stop)
+    def unapply(pos: T): Option[Symbol.Range] =
+      (pos, pos) match {
+        case (Def_Offset(start), Def_End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop))
+        case (Def_Offset(start), _) => Some(Text.Range(start, start + 1))
+        case _ => None
+      }
+  }
+
   object Item_Id
   {
     def unapply(pos: T): Option[(Long, Symbol.Range)] =