src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 32863 5e8cef567042
parent 32824 712ad8109fff
child 32865 f8d1e16ec758
equal deleted inserted replaced
32862:1fc86cec3bdf 32863:5e8cef567042
    93   type elem = Time.time * Thread.thread;
    93   type elem = Time.time * Thread.thread;
    94   fun ord ((a, _), (b, _)) = Time.compare (a, b);
    94   fun ord ((a, _), (b, _)) = Time.compare (a, b);
    95 );
    95 );
    96 
    96 
    97 fun lookup_thread xs = AList.lookup Thread.equal xs;
    97 fun lookup_thread xs = AList.lookup Thread.equal xs;
    98 fun delete_thread xs = AList.delete Thread.equal xs;
       
    99 fun update_thread xs = AList.update Thread.equal xs;
    98 fun update_thread xs = AList.update Thread.equal xs;
   100 
    99 
   101 
   100 
   102 (* state of thread manager *)
   101 (* state of thread manager *)
   103 
   102 
   119 
   118 
   120 
   119 
   121 (* unregister thread *)
   120 (* unregister thread *)
   122 
   121 
   123 fun unregister (success, message) thread = Synchronized.change state
   122 fun unregister (success, message) thread = Synchronized.change state
   124   (fn state as State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
   123   (fn state as
       
   124       State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
   125     (case lookup_thread active thread of
   125     (case lookup_thread active thread of
   126       SOME (birthtime, _, description) =>
   126       SOME (birthtime, _, description) =>
   127         let
   127         let
   128           val (group, active') =
   128           val (group, active') =
   129             if success then List.partition (fn (_, (tb, _, _)) => tb = birthtime) active
   129             if success then List.partition (fn (_, (tb, _, _)) => tb = birthtime) active
   324     handle Symtab.DUP dup => err_dup_prover dup;
   324     handle Symtab.DUP dup => err_dup_prover dup;
   325 
   325 
   326 fun print_provers thy = Pretty.writeln
   326 fun print_provers thy = Pretty.writeln
   327   (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
   327   (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
   328 
   328 
   329 fun get_prover name thy = case Symtab.lookup (Provers.get thy) name of
   329 fun get_prover name thy =
   330   NONE => NONE
   330   (case Symtab.lookup (Provers.get thy) name of
   331 | SOME (prover, _) => SOME prover;
   331     NONE => NONE
       
   332   | SOME (prover, _) => SOME prover);
       
   333 
   332 
   334 
   333 (* start prover thread *)
   335 (* start prover thread *)
   334 
   336 
   335 fun start_prover name birthtime deadtime i proof_state =
   337 fun start_prover name birthtime deadtime i proof_state =
   336   (case get_prover name (Proof.theory_of proof_state) of
   338   (case get_prover name (Proof.theory_of proof_state) of