src/Pure/General/bytes.scala
changeset 80381 00600ebb8aa3
parent 80380 94d903234f6b
child 80382 2740dec064f9
equal deleted inserted replaced
80380:94d903234f6b 80381:00600ebb8aa3
   433       case Some(s) => (false, s)
   433       case Some(s) => (false, s)
   434       case None => (true, encode_base64)
   434       case None => (true, encode_base64)
   435     }
   435     }
   436 
   436 
   437   def proper: Option[Bytes] = if (is_empty) None else Some(this)
   437   def proper: Option[Bytes] = if (is_empty) None else Some(this)
   438   def proper_text: Option[String] = if (is_empty) None else Some(text)
       
   439 
   438 
   440   def +(other: Bytes): Bytes =
   439   def +(other: Bytes): Bytes =
   441     if (other.is_empty) this
   440     if (other.is_empty) this
   442     else if (is_empty) other
   441     else if (is_empty) other
   443     else {
   442     else {