From ed09ae7a473a99c914f2af64d3387d9190e85849 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Fri, 15 Dec 2017 04:15:55 +0100
Subject: [flags] Move global time flag into an attribute.

One less global flag.
---
 stm/stm.ml               | 15 ++++++++-------
 stm/vernac_classifier.ml |  2 +-
 2 files changed, 9 insertions(+), 8 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index afb6fabcb..7045df0ed 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1935,15 +1935,16 @@ end = struct (* {{{ *)
   let vernac_interp ~solve ~abstract ~cancel_switch nworkers safe_id id
     { indentation; verbose; loc; expr = e; strlen }
   =
-    let e, time, fail =
-      let rec find ~time ~fail = function
-        | VernacTime (_,e) -> find ~time:true ~fail e
-        | VernacRedirect (_,(_,e)) -> find ~time ~fail e
-        | VernacFail e -> find ~time ~fail:true e
-        | e -> e, time, fail in find ~time:false ~fail:false e in
+    let e, time, batch, fail =
+      let rec find ~time ~batch ~fail = function
+        | VernacTime (batch,(_,e)) -> find ~time:true ~batch ~fail e
+        | VernacRedirect (_,(_,e)) -> find ~time ~batch ~fail e
+        | VernacFail e -> find ~time ~batch ~fail:true e
+        | e -> e, time, batch, fail in
+      find ~time:false ~batch:false ~fail:false e in
     let st = Vernacstate.freeze_interp_state `No in
     Vernacentries.with_fail st fail (fun () ->
-    (if time then System.with_time !Flags.time else (fun x -> x)) (fun () ->
+    (if time then System.with_time ~batch else (fun x -> x)) (fun () ->
     ignore(TaskQueue.with_n_workers nworkers (fun queue ->
     Proof_global.with_current_proof (fun _ p ->
       let goals, _, _, _, _ = Proof.proof p in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 1291b7642..2fa47ba43 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -195,7 +195,7 @@ let classify_vernac e =
   let rec static_control_classifier ~poly = function
     | VernacExpr e -> static_classifier ~poly e
     | VernacTimeout (_,e) -> static_control_classifier ~poly e
-    | VernacTime (_,e) | VernacRedirect (_, (_,e)) ->
+    | VernacTime (_,(_,e)) | VernacRedirect (_, (_,e)) ->
        static_control_classifier ~poly e
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
         (match static_control_classifier ~poly e with
-- 
cgit v1.2.3