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