# HG changeset patch
# User wenzelm
# Date 1615724519 -3600
# Node ID c7f14309e291e0bb08b0a8f125dd709e17d0c926
# Parent  8970081c6500f4c103114ead8c5b61aef88f2463
clarified signature;

diff -r 8970081c6500 -r c7f14309e291 src/HOL/Tools/ATP/system_on_tptp.ML
--- a/src/HOL/Tools/ATP/system_on_tptp.ML	Sun Mar 14 13:09:17 2021 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.ML	Sun Mar 14 13:21:59 2021 +0100
@@ -18,7 +18,7 @@
 fun list_systems () =
   let
     val url = get_url ()
-    val systems = split_lines (\<^scala>\<open>SystemOnTPTP.list_systems\<close> url)
+    val systems = trim_split_lines (\<^scala>\<open>SystemOnTPTP.list_systems\<close> url)
   in {url = url, systems = systems} end
 
 end
diff -r 8970081c6500 -r c7f14309e291 src/HOL/Tools/ATP/system_on_tptp.scala
--- a/src/HOL/Tools/ATP/system_on_tptp.scala	Sun Mar 14 13:09:17 2021 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala	Sun Mar 14 13:21:59 2021 +0100
@@ -35,12 +35,12 @@
 
   /* list systems */
 
-  def list_systems(url: URL): List[String] =
-    post_request(url, List("SubmitButton" -> "ListSystems", "ListStatus" -> "READY")).text_lines
+  def list_systems(url: URL): HTTP.Content =
+    post_request(url, List("SubmitButton" -> "ListSystems", "ListStatus" -> "READY"))
 
   object List_Systems extends Scala.Fun("SystemOnTPTP.list_systems", thread = true)
   {
     val here = Scala_Project.here
-    def apply(url: String): String = cat_lines(list_systems(Url(url)))
+    def apply(url: String): String = list_systems(Url(url)).string
   }
 }
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 =