# HG changeset patch
# User wenzelm
# Date 1743772684 -7200
# Node ID 84d5590b40c19d2e722664d8f69e3059325ee0e7
# Parent  d37f279ae3bfcd5c76bbffa9018261dd41c2ee21
clarified history: eliminate pointless var _current;

diff -r d37f279ae3bf -r 84d5590b40c1 src/Tools/jEdit/src/isabelle_navigator.scala
--- a/src/Tools/jEdit/src/isabelle_navigator.scala	Fri Apr 04 15:02:49 2025 +0200
+++ b/src/Tools/jEdit/src/isabelle_navigator.scala	Fri Apr 04 15:18:04 2025 +0200
@@ -123,23 +123,23 @@
 
   // owned by GUI thread
   private var _bypass = false
-  private var _current: Pos = Pos.none
   private var _backward = History.empty
   private var _forward = History.empty
 
+  def current: Pos = _backward.top
+  def recurrent: Pos = _forward.top
+
   override def toString: String = {
-    val size = (if (_current.defined) 1 else 0) + _backward.size + _forward.size
+    val size = _backward.size + _forward.size
     "Isabelle_Navigator(" + (if (size == 0) "" else size.toString) + ")"
   }
 
   private def convert(name: String, edit: Text.Edit): Unit = GUI_Thread.require {
-    _current = _current.convert(name, edit)
     _backward = _backward.convert(name, edit)
     _forward = _forward.convert(name, edit)
   }
 
   private def close(names: Set[String]): Unit = GUI_Thread.require {
-    if (names.contains(_current.name)) _current = Pos.none
     _backward = _backward.close(names)
     _forward = _forward.close(names)
   }
@@ -158,10 +158,9 @@
   }
 
   def record(pos: Pos): Unit = GUI_Thread.require {
-    if (!_bypass && pos.defined && !pos.equiv(_current)) {
-      _backward = _backward.push(_current)
+    if (!_bypass && pos.defined && !pos.equiv(current)) {
+      _backward = _backward.push(pos)
       _forward = History.empty
-      _current = pos
     }
   }
 
@@ -170,11 +169,11 @@
   def record(view: View): Unit = record(Pos(view))
 
   def goto_current(view: View): Unit = GUI_Thread.require {
-    if (_current.defined) {
+    if (current.defined) {
       val b = _bypass
       try {
         _bypass = true
-        PIDE.editor.goto_file(true, view, _current.name, offset = _current.offset)
+        PIDE.editor.goto_file(true, view, current.name, offset = current.offset)
       }
       finally { _bypass = b }
     }
@@ -182,26 +181,15 @@
 
   def backward(view: View): Unit = GUI_Thread.require {
     if (!_backward.is_empty) {
-      val pos0 = _current
-      val pos1 = Pos(view)
-
-      def move(pos: Pos): Unit = {
-        _forward = _forward.push(pos)
-        _current = _backward.top
-        _backward = _backward.pop
-      }
-
-      if (pos0.defined) move(pos0)
-      if (pos1.defined && !pos1.equiv(pos0)) move(pos1)
-
+      _forward = _forward.push(current).push(Pos(view))
+      _backward = _backward.pop
       goto_current(view)
     }
   }
 
   def forward(view: View): Unit = GUI_Thread.require {
     if (!_forward.is_empty) {
-      _backward = _backward.push(_current)
-      _current = _forward.top
+      _backward = _backward.push(recurrent)
       _forward = _forward.pop
       goto_current(view)
     }