accommodate OpenJDK 15;
authorwenzelm
Sat, 12 Dec 2020 12:45:21 +0100
changeset 72885 1b0f81e556a2
parent 72884 50f18a822ee9
child 72886 ac64b753a65f
accommodate OpenJDK 15;
src/Pure/Admin/build_log.scala
src/Pure/General/bytes.scala
src/Pure/General/properties.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))
     }
--- 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))