src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 36167 c1a35be8e476
parent 36143 6490319b1703
child 36181 2156a7392885
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Apr 14 21:22:48 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Apr 15 13:49:46 2010 +0200
     1.3 @@ -223,7 +223,7 @@
     1.4          do
     1.5            (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
     1.6              |> these
     1.7 -            |> List.app (unregister "Interrupted (reached timeout)");
     1.8 +            |> List.app (unregister "Timed out.");
     1.9              print_new_messages ();
    1.10              (*give threads some time to respond to interrupt*)
    1.11              OS.Process.sleep min_wait_time)
    1.12 @@ -325,7 +325,7 @@
    1.13  fun start_prover (params as {timeout, ...}) birth_time death_time i
    1.14                   relevance_override proof_state name =
    1.15    (case get_prover (Proof.theory_of proof_state) name of
    1.16 -    NONE => warning ("Unknown ATP: " ^ quote name)
    1.17 +    NONE => warning ("Unknown ATP: " ^ quote name ^ ".")
    1.18    | SOME prover =>
    1.19        let
    1.20          val {context = ctxt, facts, goal} = Proof.goal proof_state;
    1.21 @@ -357,7 +357,10 @@
    1.22    let
    1.23      val birth_time = Time.now ()
    1.24      val death_time = Time.+ (birth_time, timeout)
    1.25 -    val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *)
    1.26 +    val _ =
    1.27 +      (* RACE w.r.t. other invocations of Sledgehammer *)
    1.28 +      if null (#active (Synchronized.value global_state)) then ()
    1.29 +      else (kill_atps (); priority "Killed active Sledgehammer threads.")
    1.30      val _ = priority "Sledgehammering..."
    1.31      val _ = List.app (start_prover params birth_time death_time i
    1.32                                     relevance_override proof_state) atps