# HG changeset patch
# User blanchet
# Date 1347617367 -7200
# Node ID 8aebe857aaaa8084a900e91cfc70b660bde3186d
# Parent  838b5e8ede730dba820fe625da4dce304ea41004
merged two commands

diff -r 838b5e8ede73 -r 8aebe857aaaa NEWS
--- a/NEWS	Fri Sep 14 12:09:27 2012 +0200
+++ b/NEWS	Fri Sep 14 12:09:27 2012 +0200
@@ -126,6 +126,7 @@
   - Added MaSh relevance filter based on machine-learning; see the
     Sledgehammer manual for details.
   - Rationalized type encodings ("type_enc" option).
+  - Renamed "kill_provers" subcommand to "kill"
   - Renamed options:
       max_relevant ~> max_facts
       relevance_thresholds ~> fact_thresholds
diff -r 838b5e8ede73 -r 8aebe857aaaa src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Fri Sep 14 12:09:27 2012 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Fri Sep 14 12:09:27 2012 +0200
@@ -675,14 +675,14 @@
 currently running automatic provers, including elapsed runtime and remaining
 time until timeout.
 
-\item[\labelitemi] \textbf{\textit{kill\_provers}:} Terminates all running
-automatic provers.
+\item[\labelitemi] \textbf{\textit{kill}:} Terminates all running
+threads (automatic provers and machine learners).
 
 \item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
 ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
 \end{enum}
 
-In addition, the following subcommands provide fine control over machine
+In addition, the following subcommands provide finer control over machine
 learning with MaSh:
 
 \begin{enum}
diff -r 838b5e8ede73 -r 8aebe857aaaa src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Sep 14 12:09:27 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Sep 14 12:09:27 2012 +0200
@@ -37,9 +37,8 @@
 val minN = "min"
 val messagesN = "messages"
 val supported_proversN = "supported_provers"
-val kill_proversN = "kill_provers"
+val killN = "kill"
 val running_proversN = "running_provers"
-val kill_learnersN = "kill_learners"
 val running_learnersN = "running_learners"
 val refresh_tptpN = "refresh_tptp"
 
@@ -392,8 +391,8 @@
       messages opt_i
     else if subcommand = supported_proversN then
       supported_provers ctxt
-    else if subcommand = kill_proversN then
-      kill_provers ()
+    else if subcommand = killN then
+      (kill_provers (); kill_learners ())
     else if subcommand = running_proversN then
       running_provers ()
     else if subcommand = unlearnN then
@@ -413,8 +412,6 @@
                              ("preplay_timeout", ["0"])]))
                   fact_override (#facts (Proof.goal state))
                   (subcommand = learn_atpN orelse subcommand = relearn_atpN))
-    else if subcommand = kill_learnersN then
-      kill_learners ()
     else if subcommand = running_learnersN then
       running_learners ()
     else if subcommand = refresh_tptpN then