# HG changeset patch
# User wenzelm
# Date 1743536222 -7200
# Node ID 6ea8b99cd8d4eecc676af6b6698a22f8049da385
# Parent  49ca1a40c04a5d8e140d0d3edf601890856f7428
clarified actions and keyboard shortcuts --- requires to update jedit component;

diff -r 49ca1a40c04a -r 6ea8b99cd8d4 src/Pure/Admin/component_jedit.scala
--- a/src/Pure/Admin/component_jedit.scala	Tue Apr 01 20:59:01 2025 +0200
+++ b/src/Pure/Admin/component_jedit.scala	Tue Apr 01 21:37:02 2025 +0200
@@ -255,6 +255,10 @@
 isabelle-debugger.dock-position=floating
 isabelle-documentation.dock-position=left
 isabelle-export-browser.label=Browse theory exports
+isabelle.navigate-backwards.label=Navigate backwards
+isabelle.navigate-backwards.shortcut=AS+LEFT
+isabelle.navigate-forwards.label=Navigate forwards
+isabelle.navigate-forwards.shortcut=AS+RIGHT
 isabelle-output.dock-position=bottom
 isabelle-output.height=174
 isabelle-output.width=412
diff -r 49ca1a40c04a -r 6ea8b99cd8d4 src/Tools/jEdit/jedit_main/actions.xml
--- a/src/Tools/jEdit/jedit_main/actions.xml	Tue Apr 01 20:59:01 2025 +0200
+++ b/src/Tools/jEdit/jedit_main/actions.xml	Tue Apr 01 21:37:02 2025 +0200
@@ -2,14 +2,14 @@
 <!DOCTYPE ACTIONS SYSTEM "actions.dtd">
 
 <ACTIONS>
-	<ACTION NAME="isabelle.backward">
+	<ACTION NAME="isabelle.navigate-backwards">
 	  <CODE>
-	    isabelle.jedit.Isabelle.backward(view);
+	    isabelle.jedit.Isabelle.navigate_backwards(view);
 	  </CODE>
 	</ACTION>
-	<ACTION NAME="isabelle.forward">
+	<ACTION NAME="isabelle.navigate-forwards">
 	  <CODE>
-	    isabelle.jedit.Isabelle.forward(view);
+	    isabelle.jedit.Isabelle.navigate_forwards(view);
 	  </CODE>
 	</ACTION>
 	<ACTION NAME="isabelle.browser-info">
diff -r 49ca1a40c04a -r 6ea8b99cd8d4 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Tue Apr 01 20:59:01 2025 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Apr 01 21:37:02 2025 +0200
@@ -84,8 +84,8 @@
 
   /* navigation */
 
-  def backward(view: View): Unit = PIDE.plugin.navigator.backward(view)
-  def forward(view: View): Unit = PIDE.plugin.navigator.forward(view)
+  def navigate_backwards(view: View): Unit = PIDE.plugin.navigator.backward(view)
+  def navigate_forwards(view: View): Unit = PIDE.plugin.navigator.forward(view)
 
 
   /* text structure */