diff -r d27d1224c67f -r 7c57d9586f4c src/Pure/PIDE/resources.scala --- 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(