--- 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,