# HG changeset patch
# User wenzelm
# Date 1615635931 -3600
# Node ID 2c5d58e58fd2a00d3cbff00853d1513ddbcbd639
# Parent  22f3f2117ed7f613aa33a6ddea5c20dcdd56756e
tuned;

diff -r 22f3f2117ed7 -r 2c5d58e58fd2 src/HOL/Tools/ATP/system_on_tptp.scala
--- a/src/HOL/Tools/ATP/system_on_tptp.scala	Sat Mar 13 12:36:24 2021 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala	Sat Mar 13 12:45:31 2021 +0100
@@ -13,21 +13,26 @@
 
 object SystemOnTPTP
 {
+  /* requests */
+
   def get_url(options: Options): URL = Url(options.string("SystemOnTPTP"))
 
-  def proper_lines(text: String): List[String] =
-    Library.trim_split_lines(text).filterNot(_.startsWith("%"))
+  def post_request(url: URL, parameters: List[(String, Any)]): HTTP.Content =
+  {
+    val parameters0 =
+      List("NoHTML" -> 1, "QuietFlag" -> "-q0")
+        .filterNot(p0 => parameters.exists(p => p0._1 == p._1))
+    HTTP.Client.post(url, parameters0 ::: parameters, user_agent = "Sledgehammer")
+  }
+
+
+  /* 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] =
-  {
-    val result =
-      HTTP.Client.post(url, user_agent = "Sledgehammer", parameters =
-        List("NoHTML" -> 1,
-          "QuietFlag" -> "-q0",
-          "SubmitButton" -> "ListSystems",
-          "ListStatus" -> "READY"))
-    proper_lines(result.text)
-  }
+    proper_lines(post_request(url, List("SubmitButton" -> "ListSystems", "ListStatus" -> "READY")))
 
   object List_Systems extends Scala.Fun("SystemOnTPTP.list_systems", thread = true)
   {