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