# HG changeset patch
# User wenzelm
# Date 1699729274 -3600
# Node ID bc89bdc65f295c8cba33c475cc2afa5a0ca1c6d3
# Parent  409442cb781436a0d1b9e2ad7e630ae292049e9e
clarified signature: more operations;

diff -r 409442cb7814 -r bc89bdc65f29 src/Pure/Tools/build_cluster.scala
--- 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(
diff -r 409442cb7814 -r bc89bdc65f29 src/Pure/library.scala
--- 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]) =