Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_systems.ML
changeset 39262 bdfcf2434601
parent 39257 eec61233dbad
child 39263 e2a3c435334b 
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Sep 09 14:47:06 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Sep 09 16:06:11 2010 +0200
@@ -10,7 +10,7 @@
   datatype failure =
     Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
     OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
-    MalformedInput | MalformedOutput | UnknownError
+    MalformedInput | MalformedOutput | Interrupted | UnknownError
 
   type prover_config =
     {exec: string * string,
@@ -42,7 +42,7 @@
 datatype failure =
   Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
   SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput |
-  MalformedOutput | UnknownError
+  MalformedOutput | Interrupted | UnknownError
 
 type prover_config =
   {exec: string * string,
@@ -85,6 +85,7 @@
     "The ATP problem is malformed. Please report this to the Isabelle \
     \developers."
   | string_for_failure MalformedOutput = "The ATP output is malformed."
+  | string_for_failure Interrupted = "The ATP was interrupted."
   | string_for_failure UnknownError = "An unknown ATP error occurred."
 
 fun known_failure_in_output output =
isabelle