src/Pure/PIDE/resources.scala
changeset 77368 7c57d9586f4c
parent 77028 f5896dea6fce
--- a/src/Pure/PIDE/resources.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/PIDE/resources.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -308,8 +308,7 @@
       "Cyclic dependency of " + show_path(names)
 
     private def required_by(initiators: List[Document.Node.Name]): String =
-      if (initiators.isEmpty) ""
-      else "\n(required by " + show_path(initiators.reverse) + ")"
+      if_proper(initiators, "\n(required by " + show_path(initiators.reverse) + ")")
   }
 
   final class Dependencies[A] private(