--- 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))
}
}
}
--- 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 =