# HG changeset patch
# User wenzelm
# Date 1743770798 -7200
# Node ID 70d3ef51db666ef51407217f43b9d70539004472
# Parent  1c646ad68bd8af129777ec988666a0674027a20e
tuned source structure;

diff -r 1c646ad68bd8 -r 70d3ef51db66 src/Tools/jEdit/src/isabelle_navigator.scala
--- a/src/Tools/jEdit/src/isabelle_navigator.scala	Fri Apr 04 11:37:27 2025 +0200
+++ b/src/Tools/jEdit/src/isabelle_navigator.scala	Fri Apr 04 14:46:38 2025 +0200
@@ -180,15 +180,6 @@
     }
   }
 
-  def forward(view: View): Unit = GUI_Thread.require {
-    if (!_forward.is_empty) {
-      _backward = _backward.push(_current)
-      _current = _forward.top
-      _forward = _forward.pop
-      goto_current(view)
-    }
-  }
-
   def backward(view: View): Unit = GUI_Thread.require {
     if (!_backward.is_empty) {
       val pos0 = _current
@@ -206,4 +197,13 @@
       goto_current(view)
     }
   }
+
+  def forward(view: View): Unit = GUI_Thread.require {
+    if (!_forward.is_empty) {
+      _backward = _backward.push(_current)
+      _current = _forward.top
+      _forward = _forward.pop
+      goto_current(view)
+    }
+  }
 }