diff -r 79b4efd17d2b -r 3349e360b71d src/Pure/System/scala.scala --- a/src/Pure/System/scala.scala Wed Jun 22 11:23:53 2022 +0200 +++ b/src/Pure/System/scala.scala Wed Jun 22 13:42:30 2022 +0200 @@ -25,9 +25,8 @@ def invoke(args: List[Bytes]): List[Bytes] } - trait Fun_Single extends Fun { override def single: Boolean = true } - trait Fun_Bytes extends Fun { override def bytes: Boolean = true } - trait Fun_Single_Bytes extends Fun_Single with Fun_Bytes + trait Single_Fun extends Fun { override def single: Boolean = true } + trait Bytes_Fun extends Fun { override def bytes: Boolean = true } abstract class Fun_Strings(name: String, thread: Boolean = false) extends Fun(name, thread = thread) { @@ -37,12 +36,19 @@ } abstract class Fun_String(name: String, thread: Boolean = false) - extends Fun_Strings(name, thread = thread) with Fun_Single { + extends Fun_Strings(name, thread = thread) with Single_Fun { override def apply(args: List[String]): List[String] = List(apply(Library.the_single(args))) def apply(arg: String): String } + abstract class Fun_Bytes(name: String, thread: Boolean = false) + extends Fun(name, thread = thread) with Single_Fun with Bytes_Fun { + override def invoke(args: List[Bytes]): List[Bytes] = + List(apply(Library.the_single(args))) + def apply(arg: Bytes): Bytes + } + val encode_fun: XML.Encode.T[Fun] = { fun => import XML.Encode._ pair(string, pair(pair(bool, bool), properties))(