STM: code restructured to reuse task queue for tactics

1 files changed, 7 insertions, 0 deletions

diff --git a/lib/system.ml b/lib/system.ml
index 4188eb2b4a..59260fbf63 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -295,3 +295,10 @@ let with_time time f x =
     let msg2 = if time then "" else " (failure)" in
     msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     raise e
+
+let process_id () =
+  if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id
+  else if Flags.async_proofs_is_master () then
+    Printf.sprintf "master:%d" (Thread.id (Thread.self ()))
+  else "master"
+