# HG changeset patch
# User wenzelm
# Date 1493455848 -7200
# Node ID c41bbf657310f9542e1f740cb290c6fbf47fecbd
# Parent  e6c0afe672fa7714830cf3526c9a9c231b0c0fb9
more operations;

diff -r e6c0afe672fa -r c41bbf657310 src/Pure/General/bytes.scala
--- 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