suppress NavigatorPlugin and its dependencies -- requires to update jedit component;
authorwenzelm
Thu, 03 Apr 2025 12:52:04 +0200
changeset 82422 a54149c935bf
parent 82421 b684876ab760
child 82423 bcbbee58e7e9
suppress NavigatorPlugin and its dependencies -- requires to update jedit component;
src/Pure/Admin/component_jedit.scala
src/Tools/jEdit/src/jedit_editor.scala
--- 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) =>