more operations;

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