# HG changeset patch
# User wenzelm
# Date 1618259169 -7200
# Node ID f86661e32bed679030bb2979aad17eb5aae5ee78
# Parent  e21aef453cd492ccb938e51fd73b5d5f7a9881a8
clarified signature;

diff -r e21aef453cd4 -r f86661e32bed src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Mon Apr 12 22:18:37 2021 +0200
+++ b/src/Pure/System/scala.scala	Mon Apr 12 22:26:09 2021 +0200
@@ -39,10 +39,7 @@
   {
     override def multi: Boolean = false
     override def apply(args: List[String]): List[String] =
-      args match {
-        case List(arg) => List(apply(arg))
-        case _ => error("Expected single argument for Scala function " + quote(name))
-      }
+      List(apply(Library.the_single(args)))
     def apply(arg: String): String
   }
 
diff -r e21aef453cd4 -r f86661e32bed src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Apr 12 22:18:37 2021 +0200
+++ b/src/Pure/library.scala	Mon Apr 12 22:26:09 2021 +0200
@@ -275,6 +275,12 @@
       res.toList
     }
 
+  def the_single[A](xs: List[A]): A =
+    xs match {
+      case List(x) => x
+      case _ => error("Single argument expected")
+    }
+
 
   /* proper values */