make good use of the new precise timer...

1 files changed, 5 insertions, 7 deletions

diff --git a/moses/Timer.h b/moses/Timer.h
index e4da7fece..0471fafe1 100644
--- a/moses/Timer.h
+++ b/moses/Timer.h
@@ -20,25 +20,23 @@ class Timer
 
 private:
   bool running;
-  // note: this only has the resolution of seconds, we'd often like better resolution
-  // we make our best effort to do this on a system-by-system basis
+  bool stopped;
   double start_time;
+  double stop_time;
 
 public:
   /***
    * 'running' is initially false.  A timer needs to be explicitly started
    * using 'start'
    */
-  Timer() : running(false) {
+  Timer() : running(false),stopped(false) {
     start_time = 0;
   }
 
   void start(const char* msg = 0);
-//  void restart(const char* msg = 0);
-//  void stop(const char* msg = 0);
+  void stop(const char* msg = 0);
   void check(const char* msg = 0);
-  double get_elapsed_time();
-
+  double get_elapsed_time() const;
 };
 
 }