# HG changeset patch
# User wenzelm
# Date 1743756877 -7200
# Node ID bcbbee58e7e97c07e9617f27502e0b15517cb5a3
# Parent  a54149c935bfe96098561e8bdad57a3e92bccf5e
unused;

diff -r a54149c935bf -r bcbbee58e7e9 src/Tools/jEdit/src/isabelle_navigator.scala
--- a/src/Tools/jEdit/src/isabelle_navigator.scala	Thu Apr 03 12:52:04 2025 +0200
+++ b/src/Tools/jEdit/src/isabelle_navigator.scala	Fri Apr 04 10:54:37 2025 +0200
@@ -161,12 +161,6 @@
     buffers.iterator.foreach(_.addBufferListener(buffer_listener))
   }
 
-  def reset(): Unit = GUI_Thread.require {
-    _current = Pos.none
-    _backward = History.empty
-    _forward = History.empty
-  }
-
   def record(pos: Pos): Unit = GUI_Thread.require {
     if (!_bypass && pos.defined && !pos.equiv(_current)) {
       _backward = _backward.push(_current)