src/Pure/General/bytes.scala
changeset 65630 c41bbf657310
parent 65279 fa62e095d8f1
child 67805 2d9a265b294e
equal deleted inserted replaced
65629:e6c0afe672fa 65630:c41bbf657310
   119     if (str.contains('\uFFFD')) "Bytes(" + length + ")" else str
   119     if (str.contains('\uFFFD')) "Bytes(" + length + ")" else str
   120   }
   120   }
   121 
   121 
   122   def isEmpty: Boolean = length == 0
   122   def isEmpty: Boolean = length == 0
   123 
   123 
       
   124   def proper: Option[Bytes] = if (isEmpty) None else Some(this)
       
   125   def proper_text: Option[String] = if (isEmpty) None else Some(text)
       
   126 
   124   def +(other: Bytes): Bytes =
   127   def +(other: Bytes): Bytes =
   125     if (other.isEmpty) this
   128     if (other.isEmpty) this
   126     else if (isEmpty) other
   129     else if (isEmpty) other
   127     else {
   130     else {
   128       val new_bytes = new Array[Byte](length + other.length)
   131       val new_bytes = new Array[Byte](length + other.length)