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