clarified signature;

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

--- a/src/Pure/Thy/presentation.scala	Sat Nov 06 10:39:47 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Sat Nov 06 11:25:03 2021 +0100
@@ -495,15 +495,12 @@
       def physical_ref(
         context: Entity_Context, thy_name: String, props: Properties.T): Option[String] =
       {
-        if (thy_name == context.node.theory) {
-          for {
-            offset <- Position.Def_Offset.unapply(props)
-            end_offset <- Position.Def_End_Offset.unapply(props)
-            range = Text.Range(offset, end_offset)
-          } yield {
-            context.seen_ranges += range
-            html_context.physical_ref(range)
-          }
+        for {
+          range <- Position.Def_Range.unapply(props)
+          if thy_name == context.node.theory
+        } yield {
+          context.seen_ranges += range
+          html_context.physical_ref(range)
         }
       }