tuned signature;
authorwenzelm
Wed, 22 Jun 2022 11:23:53 +0200
changeset 75587 79b4efd17d2b
parent 75586 b2b097624e4c
child 75588 3349e360b71d
tuned signature;
src/Pure/General/bytes.scala
src/Pure/Tools/server_commands.scala
--- a/src/Pure/General/bytes.scala	Wed Jun 22 11:09:31 2022 +0200
+++ b/src/Pure/General/bytes.scala	Wed Jun 22 11:23:53 2022 +0200
@@ -42,7 +42,7 @@
 
   /* base64 */
 
-  def base64(s: String): Bytes = {
+  def decode_base64(s: String): Bytes = {
     val a = Base64.getDecoder.decode(s)
     new Bytes(a, 0, a.length)
   }
@@ -50,13 +50,13 @@
   object Decode_Base64 extends Scala.Fun("decode_base64") with Scala.Fun_Single_Bytes {
     val here = Scala_Project.here
     def invoke(args: List[Bytes]): List[Bytes] =
-      List(base64(Library.the_single(args).text))
+      List(decode_base64(Library.the_single(args).text))
   }
 
   object Encode_Base64 extends Scala.Fun("encode_base64") with Scala.Fun_Single_Bytes {
     val here = Scala_Project.here
     def invoke(args: List[Bytes]): List[Bytes] =
-      List(Bytes(Library.the_single(args).base64))
+      List(Bytes(Library.the_single(args).encode_base64))
   }
 
 
@@ -160,16 +160,16 @@
 
   def text: String = UTF8.decode_permissive(this)
 
-  def base64: String = {
+  def encode_base64: String = {
     val b =
       if (offset == 0 && length == bytes.length) bytes
       else Bytes(bytes, offset, length).bytes
     Base64.getEncoder.encodeToString(b)
   }
 
-  def maybe_base64: (Boolean, String) = {
+  def maybe_encode_base64: (Boolean, String) = {
     val s = text
-    if (this == Bytes(s)) (false, s) else (true, base64)
+    if (this == Bytes(s)) (false, s) else (true, encode_base64)
   }
 
   override def toString: String = "Bytes(" + length + ")"
--- a/src/Pure/Tools/server_commands.scala	Wed Jun 22 11:09:31 2022 +0200
+++ b/src/Pure/Tools/server_commands.scala	Wed Jun 22 11:23:53 2022 +0200
@@ -266,7 +266,7 @@
                     val matcher = Export.make_matcher(args.export_pattern)
                     for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) }
                     yield {
-                      val (base64, body) = entry.uncompressed.maybe_base64
+                      val (base64, body) = entry.uncompressed.maybe_encode_base64
                       JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
                     }
                   }))