From 4e724634839726aa11534f16e4bfb95cd81232a4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 23 Jul 2014 11:54:36 +0200
Subject: STM: code restructured to reuse task queue for tactics

---
 lib/system.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'lib/system.ml')

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"
+    
-- 
cgit v1.2.3