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