merged two commands
authorblanchet
Fri Sep 14 12:09:27 2012 +0200 (2012-09-14)
changeset 493658aebe857aaaa
parent 49364 838b5e8ede73
child 49366 3edd1c90f6e6
merged two commands
NEWS
src/Doc/Sledgehammer/document/root.tex
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     1.1 --- a/NEWS	Fri Sep 14 12:09:27 2012 +0200
     1.2 +++ b/NEWS	Fri Sep 14 12:09:27 2012 +0200
     1.3 @@ -126,6 +126,7 @@
     1.4    - Added MaSh relevance filter based on machine-learning; see the
     1.5      Sledgehammer manual for details.
     1.6    - Rationalized type encodings ("type_enc" option).
     1.7 +  - Renamed "kill_provers" subcommand to "kill"
     1.8    - Renamed options:
     1.9        max_relevant ~> max_facts
    1.10        relevance_thresholds ~> fact_thresholds
     2.1 --- a/src/Doc/Sledgehammer/document/root.tex	Fri Sep 14 12:09:27 2012 +0200
     2.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Fri Sep 14 12:09:27 2012 +0200
     2.3 @@ -675,14 +675,14 @@
     2.4  currently running automatic provers, including elapsed runtime and remaining
     2.5  time until timeout.
     2.6  
     2.7 -\item[\labelitemi] \textbf{\textit{kill\_provers}:} Terminates all running
     2.8 -automatic provers.
     2.9 +\item[\labelitemi] \textbf{\textit{kill}:} Terminates all running
    2.10 +threads (automatic provers and machine learners).
    2.11  
    2.12  \item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
    2.13  ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
    2.14  \end{enum}
    2.15  
    2.16 -In addition, the following subcommands provide fine control over machine
    2.17 +In addition, the following subcommands provide finer control over machine
    2.18  learning with MaSh:
    2.19  
    2.20  \begin{enum}
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Sep 14 12:09:27 2012 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Sep 14 12:09:27 2012 +0200
     3.3 @@ -37,9 +37,8 @@
     3.4  val minN = "min"
     3.5  val messagesN = "messages"
     3.6  val supported_proversN = "supported_provers"
     3.7 -val kill_proversN = "kill_provers"
     3.8 +val killN = "kill"
     3.9  val running_proversN = "running_provers"
    3.10 -val kill_learnersN = "kill_learners"
    3.11  val running_learnersN = "running_learners"
    3.12  val refresh_tptpN = "refresh_tptp"
    3.13  
    3.14 @@ -392,8 +391,8 @@
    3.15        messages opt_i
    3.16      else if subcommand = supported_proversN then
    3.17        supported_provers ctxt
    3.18 -    else if subcommand = kill_proversN then
    3.19 -      kill_provers ()
    3.20 +    else if subcommand = killN then
    3.21 +      (kill_provers (); kill_learners ())
    3.22      else if subcommand = running_proversN then
    3.23        running_provers ()
    3.24      else if subcommand = unlearnN then
    3.25 @@ -413,8 +412,6 @@
    3.26                               ("preplay_timeout", ["0"])]))
    3.27                    fact_override (#facts (Proof.goal state))
    3.28                    (subcommand = learn_atpN orelse subcommand = relearn_atpN))
    3.29 -    else if subcommand = kill_learnersN then
    3.30 -      kill_learners ()
    3.31      else if subcommand = running_learnersN then
    3.32        running_learners ()
    3.33      else if subcommand = refresh_tptpN then