src/Pure/Thy/presentation.scala
changeset 74714 135787601438
parent 74713 0d8b5612a0a6
child 74715 129fb11b357f
--- 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)
         }
       }