# HG changeset patch
# User wenzelm
# Date 1664651625 -7200
# Node ID 03dd2f19f1d738d3bbf44668e7df32c568ef9477
# Parent  16c12979c132a67990b357cd4d640b25e72e12d8
clarified signature: more operations;

diff -r 16c12979c132 -r 03dd2f19f1d7 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat Oct 01 20:10:56 2022 +0200
+++ b/src/Pure/General/bytes.scala	Sat Oct 01 21:13:45 2022 +0200
@@ -131,6 +131,11 @@
 
   def text: String = UTF8.decode_permissive(this)
 
+  def wellformed_text: Option[String] = {
+    val s = text
+    if (this == Bytes(s)) Some(s) else None
+  }
+
   def encode_base64: String = {
     val b =
       if (offset == 0 && length == bytes.length) bytes
@@ -138,10 +143,11 @@
     Base64.encode(b)
   }
 
-  def maybe_encode_base64: (Boolean, String) = {
-    val s = text
-    if (this == Bytes(s)) (false, s) else (true, encode_base64)
-  }
+  def maybe_encode_base64: (Boolean, String) =
+    wellformed_text match {
+      case Some(s) => (false, s)
+      case None => (true, encode_base64)
+    }
 
   override def toString: String = "Bytes(" + length + ")"