diff -r 8970081c6500 -r c7f14309e291 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Sun Mar 14 13:09:17 2021 +0100
+++ b/src/Pure/General/http.scala	Sun Mar 14 13:21:59 2021 +0100
@@ -30,8 +30,8 @@
     encoding: String = default_encoding,
     elapsed_time: Time = Time.zero)
   {
-    def text: String = new String(bytes.array, encoding)
-    def text_lines: List[String] = Library.trim_split_lines(text)
+    def string: String = new String(bytes.array, encoding)
+    def trim_split_lines: List[String] = Library.trim_split_lines(string)
   }
 
   def read_content(file: JFile): Content =