suppress NavigatorPlugin and its dependencies -- requires to update jedit component;
--- a/src/Pure/Admin/component_jedit.scala Thu Apr 03 12:37:14 2025 +0200
+++ b/src/Pure/Admin/component_jedit.scala Thu Apr 03 12:52:04 2025 +0200
@@ -89,12 +89,10 @@
private val download_plugins: List[(String, String)] =
List(
- "Code2HTML" -> "0.7",
"CommonControls" -> "1.7.4",
"Console" -> "5.1.4",
"ErrorList" -> "2.4.0",
"Highlight" -> "2.5",
- "Navigator" -> "2.7",
"SideKick" -> "1.8")
private def exclude_package(name: String): Boolean =
--- a/src/Tools/jEdit/src/jedit_editor.scala Thu Apr 03 12:37:14 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala Thu Apr 03 12:52:04 2025 +0200
@@ -121,11 +121,6 @@
GUI_Thread.require {}
PIDE.plugin.navigator.record(view)
- val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
- if (navigator != null) {
- try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) }
- catch { case _: NoSuchMethodException => }
- }
JEdit_Lib.jedit_buffer(name) match {
case Some(buffer) =>