# 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).