# HG changeset patch
# User wenzelm
# Date 1597571835 -7200
# Node ID 40b5ee5889d21124b92a9c9ea0b2a4c7991b32ca
# Parent  cafe00f2161e004f5bcb9313f92bcbe32530896b
clarified management of services: static declarations vs. dynamic instances (e.g. relevant for stateful Session.Protocol_Handler, notably Scala.Handler and session "System");

diff -r cafe00f2161e -r 40b5ee5889d2 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sat Aug 15 13:51:55 2020 +0200
+++ b/src/Pure/PIDE/session.scala	Sun Aug 16 11:57:15 2020 +0200
@@ -543,11 +543,8 @@
               prover.get.options(file_formats.prover_options(session_options))
               prover.get.init_session(resources)
 
-              Isabelle_System.services.foreach(
-                {
-                  case handler: Session.Protocol_Handler => init_protocol_handler(handler)
-                  case _ =>
-                })
+              Isabelle_System.make_services(classOf[Session.Protocol_Handler])
+                .foreach(init_protocol_handler)
 
               phase = Session.Ready
               debugger.ready()
diff -r cafe00f2161e -r 40b5ee5889d2 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Aug 15 13:51:55 2020 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sun Aug 16 11:57:15 2020 +0200
@@ -12,7 +12,7 @@
 import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
 import java.nio.file.attribute.BasicFileAttributes
 
-import scala.collection.mutable
+import scala.annotation.tailrec
 
 
 object Isabelle_System
@@ -49,7 +49,7 @@
   abstract class Service
 
   @volatile private var _settings: Option[Map[String, String]] = None
-  @volatile private var _services: Option[List[Service]] = None
+  @volatile private var _services: Option[List[Class[Service]]] = None
 
   def settings(): Map[String, String] =
   {
@@ -57,12 +57,26 @@
     _settings.get
   }
 
-  def services(): List[Service] =
+  def services(): List[Class[Service]] =
   {
     if (_services.isEmpty) init()  // unsynchronized check
     _services.get
   }
 
+  def make_services[C](c: Class[C]): List[C] =
+  {
+    @tailrec def is_subclass(c1: Class[_]): Boolean =
+    {
+      c1 == c ||
+      {
+        val c2 = c1.getSuperclass
+        c2 != null && is_subclass(c2)
+      }
+    }
+    for { c1 <- services() if is_subclass(c1) }
+      yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
+  }
+
   def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized
   {
     if (_settings.isEmpty || _services.isEmpty) {
@@ -141,10 +155,7 @@
         yield {
           def err(msg: String): Nothing =
             error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
-          try {
-            Class.forName(name).asInstanceOf[Class[Service]]
-              .getDeclaredConstructor().newInstance()
-          }
+          try { Class.forName(name).asInstanceOf[Class[Service]] }
           catch {
             case _: ClassNotFoundException => err("Class not found")
             case exn: Throwable => err(Exn.message(exn))
diff -r cafe00f2161e -r 40b5ee5889d2 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Sat Aug 15 13:51:55 2020 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Sun Aug 16 11:57:15 2020 +0200
@@ -98,7 +98,7 @@
   /* internal tools */
 
   private lazy val internal_tools: List[Isabelle_Tool] =
-    Isabelle_System.services.collect { case c: Isabelle_Scala_Tools => c.tools.toList }.flatten
+    Isabelle_System.make_services(classOf[Isabelle_Scala_Tools]).flatMap(_.tools)
 
   private def list_internal(): List[(String, String)] =
     for (tool <- internal_tools.toList)
diff -r cafe00f2161e -r 40b5ee5889d2 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Sat Aug 15 13:51:55 2020 +0200
+++ b/src/Pure/System/scala.scala	Sun Aug 16 11:57:15 2020 +0200
@@ -117,7 +117,7 @@
   }
 
   lazy val functions: List[Fun] =
-    Isabelle_System.services.collect { case c: Isabelle_Scala_Functions => c.functions.toList }.flatten
+    Isabelle_System.make_services(classOf[Isabelle_Scala_Functions]).flatMap(_.functions)
 
 
   /* invoke function */
diff -r cafe00f2161e -r 40b5ee5889d2 src/Pure/Thy/file_format.scala
--- a/src/Pure/Thy/file_format.scala	Sat Aug 15 13:51:55 2020 +0200
+++ b/src/Pure/Thy/file_format.scala	Sun Aug 16 11:57:15 2020 +0200
@@ -15,7 +15,7 @@
   /* registry */
 
   lazy val registry: Registry =
-    new Registry(Isabelle_System.services.collect { case c: File_Format => c })
+    new Registry(Isabelle_System.make_services(classOf[File_Format]))
 
   final class Registry private [File_Format](file_formats: List[File_Format])
   {
@@ -53,7 +53,7 @@
   object No_Agent extends Agent
 }
 
-trait File_Format extends Isabelle_System.Service
+abstract class File_Format extends Isabelle_System.Service
 {
   def format_name: String
   override def toString: String = "File_Format(" + format_name + ")"