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