| changeset 65630 | c41bbf657310 |
| parent 65279 | fa62e095d8f1 |
| child 67805 | 2d9a265b294e |
--- a/src/Pure/General/bytes.scala Sat Apr 29 10:37:32 2017 +0200 +++ b/src/Pure/General/bytes.scala Sat Apr 29 10:50:48 2017 +0200 @@ -121,6 +121,9 @@ def isEmpty: Boolean = length == 0 + def proper: Option[Bytes] = if (isEmpty) None else Some(this) + def proper_text: Option[String] = if (isEmpty) None else Some(text) + def +(other: Bytes): Bytes = if (other.isEmpty) this else if (isEmpty) other