# HG changeset patch
# User wenzelm
# Date 1615640905 -3600
# Node ID fc7a0ea94c4375c1908de83ebfbc6c20457cd9d2
# Parent  a114ecd280ca3ad7e21aade1c3b69ff64fa5beda
support timeout, similar to perl LWP::UserAgent;

diff -r a114ecd280ca -r fc7a0ea94c43 src/HOL/Tools/ATP/system_on_tptp.scala
--- a/src/HOL/Tools/ATP/system_on_tptp.scala	Sat Mar 13 13:44:42 2021 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala	Sat Mar 13 14:08:25 2021 +0100
@@ -17,12 +17,15 @@
 
   def get_url(options: Options): URL = Url(options.string("SystemOnTPTP"))
 
-  def post_request(url: URL, parameters: List[(String, Any)]): HTTP.Content =
+  def post_request(
+    url: URL,
+    parameters: List[(String, Any)],
+    timeout: Time = HTTP.Client.default_timeout): HTTP.Content =
   {
     val parameters0 =
-      List("NoHTML" -> 1, "QuietFlag" -> "-q0")
+      List("NoHTML" -> 1, "QuietFlag" -> "-q01")
         .filterNot(p0 => parameters.exists(p => p0._1 == p._1))
-    HTTP.Client.post(url, parameters0 ::: parameters, user_agent = "Sledgehammer")
+    HTTP.Client.post(url, parameters0 ::: parameters, timeout = timeout, user_agent = "Sledgehammer")
   }
 
 
diff -r a114ecd280ca -r fc7a0ea94c43 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Sat Mar 13 13:44:42 2021 +0100
+++ b/src/Pure/General/http.scala	Sat Mar 13 14:08:25 2021 +0100
@@ -51,10 +51,19 @@
 
   object Client
   {
-    def open_connection(url: URL, user_agent: String = ""): HttpURLConnection =
+    val default_timeout = Time.seconds(180)
+
+    def open_connection(url: URL,
+      timeout: Time = default_timeout,
+      user_agent: String = ""): HttpURLConnection =
     {
       url.openConnection match {
         case connection: HttpURLConnection =>
+          if (0 < timeout.ms && timeout.ms <= Integer.MAX_VALUE) {
+            val ms = timeout.ms.toInt
+            connection.setConnectTimeout(ms)
+            connection.setReadTimeout(ms)
+          }
           proper_string(user_agent).foreach(s => connection.setRequestProperty("User-Agent", s))
           connection
         case _ => error("Bad URL (not HTTP): " + quote(url.toString))
@@ -79,12 +88,14 @@
       })
     }
 
-    def get(url: URL, user_agent: String = ""): Content =
-      get_content(open_connection(url, user_agent = user_agent))
+    def get(url: URL, timeout: Time = default_timeout, user_agent: String = ""): Content =
+      get_content(open_connection(url, timeout = timeout, user_agent = user_agent))
 
-    def post(url: URL, parameters: List[(String, Any)], user_agent: String = ""): Content =
+    def post(url: URL, parameters: List[(String, Any)],
+      timeout: Time = default_timeout,
+      user_agent: String = ""): Content =
     {
-      val connection = open_connection(url, user_agent = user_agent)
+      val connection = open_connection(url, timeout = timeout, user_agent = user_agent)
       connection.setRequestMethod("POST")
       connection.setDoOutput(true)