--- a/src/Pure/Admin/build_log.scala Fri Dec 11 17:58:01 2020 +0100
+++ b/src/Pure/Admin/build_log.scala Sat Dec 12 12:45:21 2020 +0100
@@ -656,7 +656,7 @@
}
def uncompress_errors(bytes: Bytes, cache: XZ.Cache = XZ.cache()): List[String] =
- if (bytes.isEmpty) Nil
+ if (bytes.is_empty) Nil
else {
XML.Decode.list(YXML.string_of_body)(YXML.parse_body(bytes.uncompress(cache = cache).text))
}
--- a/src/Pure/General/bytes.scala Fri Dec 11 17:58:01 2020 +0100
+++ b/src/Pure/General/bytes.scala Sat Dec 12 12:45:21 2020 +0100
@@ -152,14 +152,12 @@
override def toString: String = "Bytes(" + length + ")"
- 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 proper: Option[Bytes] = if (is_empty) None else Some(this)
+ def proper_text: Option[String] = if (is_empty) None else Some(text)
def +(other: Bytes): Bytes =
- if (other.isEmpty) this
- else if (isEmpty) other
+ if (other.is_empty) this
+ else if (is_empty) other
else {
val new_bytes = new Array[Byte](length + other.length)
System.arraycopy(bytes, offset, new_bytes, 0, length)
--- a/src/Pure/General/properties.scala Fri Dec 11 17:58:01 2020 +0100
+++ b/src/Pure/General/properties.scala Sat Dec 12 12:45:21 2020 +0100
@@ -61,7 +61,7 @@
cache: XZ.Cache = XZ.cache(),
xml_cache: Option[XML.Cache] = None): List[T] =
{
- if (bs.isEmpty) Nil
+ if (bs.is_empty) Nil
else {
val ps =
XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress(cache = cache).text))