provide Isabelle/jEdit plugins as services, and thus allow user components do the same;

--- a/NEWS	Sat Oct 02 20:44:33 2021 +0200
+++ b/NEWS	Sat Oct 02 22:11:34 2021 +0200
@@ -49,6 +49,13 @@
 * The main plugin for Isabelle/jEdit can be deactivated and reactivated
 as documented --- was broken at least since Isabelle2018.
 
+* Add-on components may provide their own jEdit plugins, via the new
+Scala/Java module concept: instances of class
+isabelle.Scala_Project.Plugin that are declared as "services" within
+etc/build.props are activated on Isabelle/jEdit startup. E.g. see
+existing isabelle.jedit.JEdit_Plugin0 (for isabelle_jedit_base.jar) and
+isabelle.jedit.JEdit_Plugin1 (for isabelle_jedit_main.jar).
+
 
 *** Document preparation ***
 

--- a/etc/build.props	Sat Oct 02 20:44:33 2021 +0200
+++ b/etc/build.props	Sat Oct 02 22:11:34 2021 +0200
@@ -242,6 +242,7 @@
   src/Tools/jEdit/src/jedit_editor.scala \
   src/Tools/jEdit/src/jedit_lib.scala \
   src/Tools/jEdit/src/jedit_options.scala \
+  src/Tools/jEdit/src/jedit_plugins.scala \
   src/Tools/jEdit/src/jedit_rendering.scala \
   src/Tools/jEdit/src/jedit_resources.scala \
   src/Tools/jEdit/src/jedit_sessions.scala \
@@ -287,6 +288,8 @@
   isabelle.Sessions$File_Format \
   isabelle.Simplifier_Trace$Handler \
   isabelle.Tools \
+  isabelle.jedit.JEdit_Plugin0 \
+  isabelle.jedit.JEdit_Plugin1 \
   isabelle.nitpick.Kodkod$Handler \
   isabelle.nitpick.Scala_Functions \
   isabelle.spark.SPARK$Load_Command1 \

--- a/src/Pure/Tools/scala_project.scala	Sat Oct 02 20:44:33 2021 +0200
+++ b/src/Pure/Tools/scala_project.scala	Sat Oct 02 22:11:34 2021 +0200
@@ -22,15 +22,21 @@
   }
 
 
-  /* file and directories */
+  /* plugins: modules with dynamic build */
 
-  def plugin_contexts(): List[Scala_Build.Context] =
-    for (plugin <- List("jedit_base", "jedit_main"))
-    yield Scala_Build.context(Path.explode("$ISABELLE_HOME/src/Tools/jEdit") + Path.basic(plugin))
+  class Plugin(dir: Path) extends Isabelle_System.Service
+  {
+    def context(): Scala_Build.Context = Scala_Build.context(dir)
+  }
+
+  lazy val plugins: List[Plugin] = Isabelle_System.make_services(classOf[Plugin])
+
+
+  /* file and directories */
 
   lazy val isabelle_files: (List[Path], List[Path]) =
   {
-    val contexts = Scala_Build.component_contexts() ::: plugin_contexts()
+    val contexts = Scala_Build.component_contexts() ::: plugins.map(_.context())
 
     val jars1 = Path.split(Isabelle_System.getenv("ISABELLE_CLASSPATH"))
     val jars2 = contexts.flatMap(_.requirements)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit_plugins.scala	Sat Oct 02 22:11:34 2021 +0200
@@ -0,0 +1,16 @@
+/*  Title:      Tools/jEdit/src/jedit_plugin.scala
+    Author:     Makarius
+
+Isabelle/jEdit plugins via dynamic Isabelle/Scala/Java modules.
+*/
+
+package isabelle.jedit
+
+import isabelle._
+
+
+class JEdit_Plugin0 extends
+  Scala_Project.Plugin(Path.explode("$ISABELLE_HOME/src/Tools/jEdit/jedit_base"))
+
+class JEdit_Plugin1 extends
+  Scala_Project.Plugin(Path.explode("$ISABELLE_HOME/src/Tools/jEdit/jedit_main"))

--- a/src/Tools/jEdit/src/main.scala	Sat Oct 02 20:44:33 2021 +0200
+++ b/src/Tools/jEdit/src/main.scala	Sat Oct 02 22:11:34 2021 +0200
@@ -82,7 +82,7 @@
 </PERSPECTIVE>""")
           }
 
-          Scala_Project.plugin_contexts().foreach(_.build())
+          for (plugin <- Scala_Project.plugins) { plugin.context().build() }
 
 
           /* args */