Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
only kill ATP threads in nonblocking mode
authorblanchet
Wed, 01 Sep 2010 18:47:07 +0200
changeset 39000 d73a054e018c
parent 38999 8223d0f8f5cc
child 39001 42e6eb597c30
only kill ATP threads in nonblocking mode
src/HOL/Tools/Sledgehammer/sledgehammer.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 01 18:42:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 01 18:47:07 2010 +0200
@@ -394,7 +394,7 @@
       let
         val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
         val thy = Proof.theory_of state
-        val _ = kill_atps ()
+        val _ = () |> not blocking ? kill_atps
         val _ = priority "Sledgehammering..."
         val (_, hyp_ts, concl_t) = strip_subgoal goal i
         val provers = map (`(get_prover thy)) atps
isabelle