# HG changeset patch
# User wenzelm
# Date 1598525517 -7200
# Node ID 5924c1da3c45d42739a871ff6dcfa98258fcd1af
# Parent  6157757bb13330e218dd31aee154003f5c261b07
clarified modules;

diff -r 6157757bb133 -r 5924c1da3c45 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Aug 27 12:43:06 2020 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Aug 27 12:51:57 2020 +0200
@@ -64,18 +64,8 @@
   }
 
   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) }
+    for { c1 <- services() if Library.is_subclass(c1, c) }
       yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
-  }
 
   def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized
   {
diff -r 6157757bb133 -r 5924c1da3c45 src/Pure/library.scala
--- a/src/Pure/library.scala	Thu Aug 27 12:43:06 2020 +0200
+++ b/src/Pure/library.scala	Thu Aug 27 12:51:57 2020 +0200
@@ -276,4 +276,20 @@
 
   def proper_list[A](list: List[A]): Option[List[A]] =
     if (list == null || list.isEmpty) None else Some(list)
+
+
+  /* reflection */
+
+  def is_subclass[A, B](a: Class[A], b: Class[B]): Boolean =
+  {
+    @tailrec def subclass(c: Class[_]): Boolean =
+    {
+      c == b ||
+        {
+          val d = c.getSuperclass
+          d != null && subclass(d)
+        }
+    }
+    subclass(a)
+  }
 }