clarified signature: let Sledgehammer handle SystemOnTPTP comments;

--- a/src/HOL/Tools/ATP/system_on_tptp.scala	Sat Mar 13 14:27:34 2021 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala	Sat Mar 13 14:55:27 2021 +0100
@@ -35,11 +35,8 @@
 
   /* list systems */
 
-  def proper_lines(content: HTTP.Content): List[String] =
-    Library.trim_split_lines(content.text).filterNot(_.startsWith("%"))
-
   def list_systems(url: URL): List[String] =
-    proper_lines(post_request(url, List("SubmitButton" -> "ListSystems", "ListStatus" -> "READY")))
+    post_request(url, List("SubmitButton" -> "ListSystems", "ListStatus" -> "READY")).text_lines
 
   object List_Systems extends Scala.Fun("SystemOnTPTP.list_systems", thread = true)
   {

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