clarified signature: more operations;

--- a/src/Pure/Tools/build_cluster.scala	Sat Nov 11 19:36:59 2023 +0100
+++ b/src/Pure/Tools/build_cluster.scala	Sat Nov 11 20:01:14 2023 +0100
@@ -88,6 +88,9 @@
           options = options)
       }
     }
+
+    def parse_single(str: String): Host =
+      Library.the_single(parse(str), "Single host expected: " + quote(str))
   }
 
   class Host(

--- a/src/Pure/library.scala	Sat Nov 11 19:36:59 2023 +0100
+++ b/src/Pure/library.scala	Sat Nov 11 20:01:14 2023 +0100
@@ -278,10 +278,10 @@
       res.toList
     }
 
-  def the_single[A](xs: List[A]): A =
+  def the_single[A](xs: List[A], message: => String = "Single argument expected"): A =
     xs match {
       case List(x) => x
-      case _ => error("Single argument expected")
+      case _ => error(message)
     }
 
   def symmetric_difference[A](xs: List[A], ys: List[A]): (List[A], List[A]) =