--- 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()
}
--- 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))(