clarified signature;
authorwenzelm
Wed, 22 Jun 2022 13:42:30 +0200
changeset 75588 3349e360b71d
parent 75587 79b4efd17d2b
child 75589 3bee51daf9a9
clarified signature;
src/Pure/General/bytes.scala
src/Pure/System/scala.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()
   }
 
 
--- 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))(