# HG changeset patch # User wenzelm # Date 1368783352 -7200 # Node ID 9003b293e775592d6dc2f9003d8eed184f1eefb2 # Parent 0476162187c484920f4dc2adca01efc12016689e tuned signature -- emphasize thread creation here; diff -r 0476162187c4 -r 9003b293e775 src/HOL/Tools/Sledgehammer/async_manager.ML --- a/src/HOL/Tools/Sledgehammer/async_manager.ML Fri May 17 11:05:59 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Fri May 17 11:35:52 2013 +0200 @@ -9,7 +9,7 @@ signature ASYNC_MANAGER = sig val break_into_chunks : string -> string list - val launch : + val thread : string -> Time.time -> Time.time -> string * string -> (unit -> bool * string) -> unit val kill_threads : string -> string -> unit @@ -180,7 +180,7 @@ check_thread_manager ()) -fun launch tool birth_time death_time desc f = +fun thread tool birth_time death_time desc f = (Toplevel.thread true (fn () => let diff -r 0476162187c4 -r 9003b293e775 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri May 17 11:05:59 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri May 17 11:35:52 2013 +0200 @@ -883,7 +883,7 @@ val birth_time = Time.now () val death_time = Time.+ (birth_time, hard_timeout) val desc = ("Machine learner for Sledgehammer", "") - in Async_Manager.launch MaShN birth_time death_time desc task end + in Async_Manager.thread MaShN birth_time death_time desc task end fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) prover t facts used_ths = diff -r 0476162187c4 -r 9003b293e775 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 17 11:05:59 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 17 11:35:52 2013 +0200 @@ -157,7 +157,7 @@ (outcome_code, state) end else - (Async_Manager.launch SledgehammerN birth_time death_time (desc ()) + (Async_Manager.thread SledgehammerN birth_time death_time (desc ()) ((fn (outcome_code, message) => (verbose orelse outcome_code = someN, message ())) o go);