src/Pure/General/http.scala
changeset 73425 d0f529d5c5c9
parent 73422 fc7a0ea94c43
child 73429 8970081c6500
--- a/src/Pure/General/http.scala	Sat Mar 13 14:27:34 2021 +0100
+++ b/src/Pure/General/http.scala	Sat Mar 13 14:55:27 2021 +0100
@@ -30,6 +30,7 @@
     encoding: String = default_encoding)
   {
     def text: String = new String(bytes.array, encoding)
+    def text_lines: List[String] = Library.trim_split_lines(text)
   }
 
   def read_content(file: JFile): Content =