From a758aac39aa330911f5f589ab3cae1bebed1e9ce Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 10 Jun 2017 04:12:11 +0200
Subject: [stm] Move process_id to Spawned.

This brings us one step closer to actually moving all STM flags to
`stm`.
---
 stm/asyncTaskQueue.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'stm/asyncTaskQueue.ml')

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


From 50159f9c1748ccf1d66341d171081a998d116d2f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 10 Jun 2017 04:27:21 +0200
Subject: [flags] [stm] Reorganize flags.

We move the main async flags to the STM in preparation for
more state encapsulation.

There is still more work to do, in particular we should make some of
the defaults a parameter instead of a flag.
---
 stm/asyncTaskQueue.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'stm/asyncTaskQueue.ml')

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 28c16a656a..26aef53552 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -11,10 +11,10 @@ open Pp
 open Util
 
 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 ()
 
 type cancel_switch = bool ref
+let async_proofs_flags_for_workers = ref []
 
 module type Task = sig
 
@@ -117,12 +117,12 @@ module Make(T : Task) () = struct
     let name = Printf.sprintf "%s:%d" !T.name id in
     let proc, ic, oc =
       let rec set_slave_opt = function
-        | [] -> !Flags.async_proofs_flags_for_workers @
+        | [] -> !async_proofs_flags_for_workers @
                 ["-toploop"; !T.name^"top";
                  "-worker-id"; name;
                  "-async-proofs-worker-priority";
-                   Flags.string_of_priority !Flags.async_proofs_worker_priority]
-        | ("-ideslave"|"-emacs"|"-batch")::tl -> set_slave_opt tl
+                   CoqworkmgrApi.(string_of_priority !WorkerLoop.async_proofs_worker_priority)]
+        | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
         | ("-async-proofs" |"-toploop" |"-vio2vo"
           |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv"
           |"-compile" |"-compile-verbose"
-- 
cgit v1.2.3