# HG changeset patch
# User wenzelm
# Date 1743627574 -7200
# Node ID 7b98d2a8ee6ecc473804c2c0e5d78ae42d40ac6f
# Parent  eaf11864fb71d5beecedd7f815c50b38a37b6fae
unused (see also 1046a69fabaa);

diff -r eaf11864fb71 -r 7b98d2a8ee6e src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Apr 02 22:09:45 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Apr 02 22:59:34 2025 +0200
@@ -219,20 +219,6 @@
       override def toString: String = "file " + quote(pos.name)
     }
 
-  def hyperlink_model(focus: Boolean, model: Document_Model, offset: Text.Offset): Hyperlink =
-    model match {
-      case file_model: File_Model =>
-        val pos =
-          try { file_model.node_position(offset) }
-          catch { case ERROR(_) => Line.Node_Position(file_model.node_name.node) }
-        hyperlink_file(focus, pos)
-      case buffer_model: Buffer_Model =>
-        new Hyperlink {
-          def follow(view: View): Unit = goto_buffer(focus, view, buffer_model.buffer, offset)
-          override def toString: String = "buffer " + quote(model.node_name.node)
-        }
-    }
-
   def hyperlink_source_file(
     focus: Boolean,
     source_name: String,