# HG changeset patch
# User blanchet
# Date 1306230959 -7200
# Node ID 05d1dc9fefdb8c9baa4d7fd809641e3a3bcde08e
# Parent  10baeee358a50cffd83d6c023371e3b42c9988ec
added quietness flag

diff -r 10baeee358a5 -r 05d1dc9fefdb src/HOL/Tools/ATP/scripts/remote_atp
--- a/src/HOL/Tools/ATP/scripts/remote_atp	Tue May 24 10:03:15 2011 +0200
+++ b/src/HOL/Tools/ATP/scripts/remote_atp	Tue May 24 11:55:59 2011 +0200
@@ -25,7 +25,7 @@
 
 #----Get format and transform options if specified
 my %Options;
-getopts("hws:t:c:",\%Options);
+getopts("hws:t:c:q:",\%Options);
 
 #----Usage
 sub usage() {
@@ -36,6 +36,7 @@
   print("    -s<system>      ATP to use\n");
   print("    -t<time_limit>  CPU time limit for ATP\n");
   print("    -c<command>     custom ATP invocation command\n");
+  print("    -q<num>         quietness level (0 = most verbose, 3 = least verbose)\n");
   print("    <file_name>     TPTP problem file\n");
   exit(0);
 }
@@ -72,6 +73,10 @@
 if (exists($Options{'c'})) {
     $URLParameters{"Command___$System"} = $Options{'c'};
 }
+#----Quietness
+if (exists($Options{'q'})) {
+    $URLParameters{"QuietFlag"} = "-q" . $Options{'q'};
+}
 
 #----Get single file name
 if (exists($URLParameters{"ProblemSource"})) {