# HG changeset patch
# User wenzelm
# Date 1615643727 -3600
# Node ID d0f529d5c5c9f0aa53f0638604f71a8eb7b6f3b9
# Parent  2b657a70116cd0fcd80cfd6234787ae0b20effac
clarified signature: let Sledgehammer handle SystemOnTPTP comments;

diff -r 2b657a70116c -r d0f529d5c5c9 src/HOL/Tools/ATP/system_on_tptp.scala
--- 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)
   {
diff -r 2b657a70116c -r d0f529d5c5c9 src/Pure/General/http.scala
--- 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 =