# HG changeset patch
# User wenzelm
# Date 1607773521 -3600
# Node ID 1b0f81e556a2d4f0331d798e7218ad0ec0cc37fc
# Parent  50f18a822ee9bffc6cb0710d097e8bea8d217572
accommodate OpenJDK 15;

diff -r 50f18a822ee9 -r 1b0f81e556a2 src/Pure/Admin/build_log.scala
--- 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))
     }
diff -r 50f18a822ee9 -r 1b0f81e556a2 src/Pure/General/bytes.scala
--- 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)
diff -r 50f18a822ee9 -r 1b0f81e556a2 src/Pure/General/properties.scala
--- 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))