# HG changeset patch
# User wenzelm
# Date 1743624585 -7200
# Node ID eaf11864fb71d5beecedd7f815c50b38a37b6fae
# Parent  e9ec8daa788801f9b792dbbb6852bfda02b97faa
prefer generic action names, to be injected into jEdit codebase eventually;

diff -r e9ec8daa7888 -r eaf11864fb71 src/Pure/Admin/component_jedit.scala
--- a/src/Pure/Admin/component_jedit.scala	Wed Apr 02 21:52:54 2025 +0200
+++ b/src/Pure/Admin/component_jedit.scala	Wed Apr 02 22:09:45 2025 +0200
@@ -255,10 +255,6 @@
 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
@@ -344,6 +340,10 @@
 metal.primary.fontsize=12
 metal.secondary.font=Isabelle DejaVu Sans
 metal.secondary.fontsize=12
+navigate-backwards.label=Navigate backwards
+navigate-backwards.shortcut=AS+LEFT
+navigate-forwards.label=Navigate forwards
+navigate-forwards.shortcut=AS+RIGHT
 navigator.showOnToolbar=true
 new-file-in-mode.shortcut=
 next-bracket.shortcut2=C+e C+9
diff -r e9ec8daa7888 -r eaf11864fb71 src/Tools/jEdit/jedit_main/actions.xml
--- a/src/Tools/jEdit/jedit_main/actions.xml	Wed Apr 02 21:52:54 2025 +0200
+++ b/src/Tools/jEdit/jedit_main/actions.xml	Wed Apr 02 22:09:45 2025 +0200
@@ -2,12 +2,12 @@
 <!DOCTYPE ACTIONS SYSTEM "actions.dtd">
 
 <ACTIONS>
-	<ACTION NAME="isabelle.navigate-backwards">
+	<ACTION NAME="navigate-backwards">
 	  <CODE>
 	    isabelle.jedit.Isabelle.navigate_backwards(view);
 	  </CODE>
 	</ACTION>
-	<ACTION NAME="isabelle.navigate-forwards">
+	<ACTION NAME="navigate-forwards">
 	  <CODE>
 	    isabelle.jedit.Isabelle.navigate_forwards(view);
 	  </CODE>