# HG changeset patch
# User wenzelm
# Date 1615805036 -3600
# Node ID 3696bb4085ed0959a0f0efa3a967cbea9fffdabe
# Parent  cb127ce2c092ccceb6e8d54cf3c31429fa63658e
tuned signature (again);

diff -r cb127ce2c092 -r 3696bb4085ed src/HOL/Tools/ATP/system_on_tptp.scala
--- a/src/HOL/Tools/ATP/system_on_tptp.scala	Sun Mar 14 22:55:52 2021 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala	Mon Mar 15 11:43:56 2021 +0100
@@ -41,7 +41,7 @@
   object List_Systems extends Scala.Fun("SystemOnTPTP.list_systems", thread = true)
   {
     val here = Scala_Project.here
-    def apply(url: String): String = list_systems(Url(url)).string
+    def apply(url: String): String = list_systems(Url(url)).text
   }
 
 
@@ -76,11 +76,14 @@
       val problem = File.read(Path.explode(problem_path))
       val res = run_system(Url(url), system, problem, extra = extra, timeout = Time.ms(timeout))
 
+      val text = res.text
+      val timing = res.elapsed_time.ms
+
       val bad_prover = "WARNING: " + system + " does not exist"
-      if (res.trim_split_lines.exists(_.startsWith(bad_prover))) {
+      if (split_lines(text).exists(_.startsWith(bad_prover))) {
         error("The ATP " + quote(system) + " is not available at SystemOnTPTP")
       }
-      else Library.cat_strings0(List(res.string, res.elapsed_time.ms.toString))
+      else Library.cat_strings0(List(text, timing.toString))
     }
   }
 }
diff -r cb127ce2c092 -r 3696bb4085ed src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Sun Mar 14 22:55:52 2021 +0100
+++ b/src/Pure/General/http.scala	Mon Mar 15 11:43:56 2021 +0100
@@ -30,8 +30,7 @@
     encoding: String = default_encoding,
     elapsed_time: Time = Time.zero)
   {
-    def string: String = new String(bytes.array, encoding)
-    def trim_split_lines: List[String] = Library.trim_split_lines(string)
+    def text: String = new String(bytes.array, encoding)
   }
 
   def read_content(file: JFile): Content =