# HG changeset patch # User wenzelm # Date 1636194303 -3600 # Node ID 1357876014383e5a0d9b93e4f5847cec50f04eb6 # Parent 0d8b5612a0a6b2c3f1eec65712f3ee6c239c8992 clarified signature; 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)] = diff -r 0d8b5612a0a6 -r 135787601438 src/Pure/Thy/presentation.scala --- 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) } }