--- 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) }
}