# HG changeset patch
# User wenzelm
# Date 1615642027 -3600
# Node ID 53cba4441cfbe5b5c6248eb7d03308ba7b3ad4f3
# Parent  fc7a0ea94c4375c1908de83ebfbc6c20457cd9d2
clarified error;

diff -r fc7a0ea94c43 -r 53cba4441cfb src/HOL/Tools/ATP/system_on_tptp.scala
--- a/src/HOL/Tools/ATP/system_on_tptp.scala	Sat Mar 13 14:08:25 2021 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala	Sat Mar 13 14:27:07 2021 +0100
@@ -25,7 +25,11 @@
     val parameters0 =
       List("NoHTML" -> 1, "QuietFlag" -> "-q01")
         .filterNot(p0 => parameters.exists(p => p0._1 == p._1))
-    HTTP.Client.post(url, parameters0 ::: parameters, timeout = timeout, user_agent = "Sledgehammer")
+    try {
+      HTTP.Client.post(url, parameters0 ::: parameters,
+        timeout = timeout, user_agent = "Sledgehammer")
+    }
+    catch { case ERROR(msg) => cat_error("Failed to access SystemOnTPTP server", msg) }
   }