unused (see also 1046a69fabaa);
authorwenzelm
Wed, 02 Apr 2025 22:59:34 +0200
changeset 82416 7b98d2a8ee6e
parent 82415 eaf11864fb71
child 82417 9f0f37a12ea8
unused (see also 1046a69fabaa);
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,