# HG changeset patch # User wenzelm # Date 1739897317 -3600 # Node ID 355a2c1cdf401c34add1e79118ee2d1cc5e4b789 # Parent 7dc4aa4078995736384e6cd666245dea5e216e17 tuned signature: emphasize semantics; diff -r 7dc4aa407899 -r 355a2c1cdf40 src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Tue Feb 18 17:16:55 2025 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Feb 18 17:48:37 2025 +0100 @@ -238,12 +238,12 @@ line1: Int, offset: Symbol.Offset ) : Option[Hyperlink] = { - for (name <- PIDE.resources.source_file(source_name)) yield { + for (platform_path <- PIDE.resources.source_file(source_name)) yield { def hyperlink(pos: Line.Position) = - hyperlink_file(focus, Line.Node_Position(name, pos)) + hyperlink_file(focus, Line.Node_Position(platform_path, pos)) if (offset > 0) { - PIDE.resources.get_file_content(PIDE.resources.node_name(name)) match { + PIDE.resources.get_file_content(PIDE.resources.node_name(platform_path)) match { case Some(text) => hyperlink( Symbol.iterator(text).zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1).