src/Tools/jEdit/src/jedit_editor.scala

--- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Jan 08 17:53:44 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Jan 08 19:08:26 2017 +0100
@@ -250,19 +250,22 @@
     : Option[Hyperlink] =
   {
     for (name <- PIDE.resources.source_file(source_name)) yield {
-      JEdit_Lib.jedit_buffer(name) match {
-        case Some(buffer) if offset > 0 =>
-          val pos =
-            JEdit_Lib.buffer_lock(buffer) {
+      def hyperlink(pos: Line.Position) =
+        hyperlink_file(focus, Line.Node_Position(name, pos))
+
+      if (offset > 0) {
+        PIDE.resources.get_file_content(PIDE.resources.node_name(name)) match {
+          case Some(text) =>
+            hyperlink(
               (Line.Position.zero /:
-                (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
+                (Symbol.iterator(text).
                   zipWithIndex.takeWhile(p => p._2 < offset - 1).
-                  map(_._1)))(_.advance(_, Text.Length))
-            }
-          hyperlink_file(focus, Line.Node_Position(name, pos))
-        case _ =>
-          hyperlink_file(focus, Line.Node_Position(name, Line.Position((line1 - 1) max 0)))
+                  map(_._1)))(_.advance(_, Text.Length)))
+          case None =>
+            hyperlink(Line.Position((line1 - 1) max 0))
+        }
       }
+      else hyperlink(Line.Position((line1 - 1) max 0))
     }
   }