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.
---
 lib/flags.ml   |  2 --
 lib/flags.mli  |  3 ---
 lib/system.ml  | 10 +++++-----
 lib/system.mli |  2 +-
 4 files changed, 6 insertions(+), 11 deletions(-)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index 644f66d02..cd4a22d58 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -48,8 +48,6 @@ let profile = false
 let ide_slave = ref false
 let ideslave_coqtop_flags = ref None
 
-let time = ref false
-
 let raw_print = ref false
 
 let univ_print = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 000862b2c..62328e3d3 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -35,9 +35,6 @@ val profile : bool
 val ide_slave : bool ref
 val ideslave_coqtop_flags : string option ref
 
-(* -time option: every command will be wrapped with `Time` *)
-val time : bool ref
-
 (* development flag to detect race conditions, it should go away. *)
 val we_are_parsing : bool ref
 
diff --git a/lib/system.ml b/lib/system.ml
index 2c8dbac7c..e56736eb1 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -294,18 +294,18 @@ let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) =
   real (round (sstop -. sstart)) ++ str "s" ++
   str ")"
 
-let with_time time f x =
+let with_time ~batch f x =
   let tstart = get_time() in
-  let msg = if time then "" else "Finished transaction in " in
+  let msg = if batch then "" else "Finished transaction in " in
   try
     let y = f x in
     let tend = get_time() in
-    let msg2 = if time then "" else " (successful)" in
+    let msg2 = if batch then "" else " (successful)" in
     Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     y
   with e ->
     let tend = get_time() in
-    let msg = if time then "" else "Finished failing transaction in " in
-    let msg2 = if time then "" else " (failure)" in
+    let msg = if batch then "" else "Finished failing transaction in " in
+    let msg2 = if batch then "" else " (failure)" in
     Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     raise e
diff --git a/lib/system.mli b/lib/system.mli
index c02bc9c8a..0c0cc9fae 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -104,4 +104,4 @@ val get_time : unit -> time
 val time_difference : time -> time -> float (** in seconds *)
 val fmt_time_difference : time -> time -> Pp.t
 
-val with_time : bool -> ('a -> 'b) -> 'a -> 'b
+val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b
-- 
cgit v1.2.3