[stm] Move process_id to Spawned.

This brings us one step closer to actually moving all STM flags to
`stm`.

6 files changed, 13 insertions, 14 deletions

diff --git a/lib/system.ml b/lib/system.ml
index 4b5066ef41..2c8dbac7c0 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -309,9 +309,3 @@ let with_time time f x =
     let msg2 = if time then "" else " (failure)" in
     Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     raise e
-
-let process_id () =
-  Printf.sprintf "%d:%s:%d" (Unix.getpid ())
-    (if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id
-     else "master")
-    (Thread.id (Thread.self ()))
diff --git a/lib/system.mli b/lib/system.mli
index aa964abebe..c02bc9c8ac 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -105,6 +105,3 @@ val time_difference : time -> time -> float (** in seconds *)
 val fmt_time_difference : time -> time -> Pp.t
 
 val with_time : bool -> ('a -> 'b) -> 'a -> 'b
-
-(** {6 Name of current process.} *)
-val process_id : unit -> string
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index cd22a71835..28c16a656a 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -10,7 +10,7 @@ open CErrors
 open Pp
 open Util
 
-let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (System.process_id ()) Pp.pp_with pp
+let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp
 
 let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else ()
 
@@ -295,7 +295,7 @@ module Make(T : Task) () = struct
   let slave_handshake () =
     Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc)
 
-  let pp_pid pp = Pp.(str (System.process_id () ^ " ") ++ pp)
+  let pp_pid pp = Pp.(str (Spawned.process_id () ^ " ") ++ pp)
 
   let debug_with_pid = Feedback.(function
     | { contents = Message(Debug, loc, pp) } as fb ->
diff --git a/stm/spawned.ml b/stm/spawned.ml
index 6ab096abf9..fb5708f3a3 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -73,3 +73,9 @@ let get_channels () =
     Printf.eprintf "Fatal error: ideslave communication channels not set.\n";
     exit 1
   | Some(ic, oc) -> ic, oc
+
+let process_id () =
+  Printf.sprintf "%d:%s:%d" (Unix.getpid ())
+    (if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id
+     else "master")
+    (Thread.id (Thread.self ()))
diff --git a/stm/spawned.mli b/stm/spawned.mli
index c3cf4d67b0..7f463c6a6e 100644
--- a/stm/spawned.mli
+++ b/stm/spawned.mli
@@ -20,3 +20,5 @@ val init_channels : unit -> unit
 (* Once initialized, these are the channels to talk with our master *)
 val get_channels : unit -> CThread.thread_ic * out_channel
 
+(** {6 Name of current process.} *)
+val process_id : unit -> string
diff --git a/stm/stm.ml b/stm/stm.ml
index 8aa832da84..8772630964 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -10,8 +10,8 @@
 (* let stm_debug () = !Flags.debug *)
 let stm_debug () = !Flags.stm_debug
 
-let stm_pr_err s  = Format.eprintf "%s] %s\n%!"     (System.process_id ()) s
-let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (System.process_id ()) Pp.pp_with pp
+let stm_pr_err s  = Format.eprintf "%s] %s\n%!"     (Spawned.process_id ()) s
+let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp
 
 let stm_prerr_endline s = if stm_debug () then begin stm_pr_err (s ()) end else ()
 let stm_pperr_endline s = if stm_debug () then begin stm_pp_err (s ()) end else ()
@@ -355,7 +355,7 @@ end = struct (* {{{ *)
     if stm_debug () then Flags.we_are_parsing := false;
 
     let fname =
-      "stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in
+      "stm_" ^ Str.global_replace (Str.regexp " ") "_" (Spawned.process_id ()) in
     let string_of_transaction = function
       | Cmd { cast = t } | Fork (t, _,_,_) ->
           (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR")