# HG changeset patch # User blanchet # Date 1329242313 -3600 # Node ID 24990fae5f920f2faed44bef2c481388552d7253 # Parent 837f79bdd3c4a20294fc14a302c3eff6296fb4ff better error message diff -r 837f79bdd3c4 -r 24990fae5f92 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Feb 14 17:59:10 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Feb 14 18:58:33 2012 +0100 @@ -493,10 +493,15 @@ fun the_system name versions = case get_system name versions of (SOME sys, _) => sys - | (NONE, []) => error ("SystemOnTPTP is currently not available.") + | (NONE, []) => error ("SystemOnTPTP is not available.") | (NONE, syss) => - error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^ - "(Available systems: " ^ commas_quote syss ^ ".)") + case syss |> filter_out (String.isPrefix "%") + |> filter_out (curry (op =) "") of + [] => error ("SystemOnTPTP is not available.") + | [msg] => error ("SystemOnTPTP is not available: " ^ msg ^ ".") + | syss => + error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^ + "(Available systems: " ^ commas_quote syss ^ ".)") val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)