# HG changeset patch # User wenzelm # Date 1655898150 -7200 # Node ID 3349e360b71d1a04a11a698846fd771912c3bb01 # Parent 79b4efd17d2b3c9bba917562a06cabc06595745b clarified signature; diff -r 79b4efd17d2b -r 3349e360b71d src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Wed Jun 22 11:23:53 2022 +0200 +++ b/src/Pure/General/bytes.scala Wed Jun 22 13:42:30 2022 +0200 @@ -47,31 +47,27 @@ new Bytes(a, 0, a.length) } - object Decode_Base64 extends Scala.Fun("decode_base64") with Scala.Fun_Single_Bytes { + object Decode_Base64 extends Scala.Fun_Bytes("decode_base64") { val here = Scala_Project.here - def invoke(args: List[Bytes]): List[Bytes] = - List(decode_base64(Library.the_single(args).text)) + def apply(arg: Bytes): Bytes = decode_base64(arg.text) } - object Encode_Base64 extends Scala.Fun("encode_base64") with Scala.Fun_Single_Bytes { + object Encode_Base64 extends Scala.Fun_Bytes("encode_base64") { val here = Scala_Project.here - def invoke(args: List[Bytes]): List[Bytes] = - List(Bytes(Library.the_single(args).encode_base64)) + def apply(arg: Bytes): Bytes = Bytes(arg.encode_base64) } /* XZ compression */ - object Compress extends Scala.Fun("compress") with Scala.Fun_Single_Bytes { + object Compress extends Scala.Fun_Bytes("compress") { val here = Scala_Project.here - def invoke(args: List[Bytes]): List[Bytes] = - List(Library.the_single(args).compress()) + def apply(arg: Bytes): Bytes = arg.compress() } - object Uncompress extends Scala.Fun("uncompress") with Scala.Fun_Single_Bytes { + object Uncompress extends Scala.Fun_Bytes("uncompress") { val here = Scala_Project.here - def invoke(args: List[Bytes]): List[Bytes] = - List(Library.the_single(args).uncompress()) + def apply(arg: Bytes): Bytes = arg.uncompress() } 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))(