diff -r b94037830dc8 -r 63ccf7136641 src/lemon/time_measure.h
--- a/src/lemon/time_measure.h	Wed Nov 17 19:56:46 2004 +0000
+++ b/src/lemon/time_measure.h	Wed Nov 17 22:18:30 2004 +0000
@@ -71,7 +71,7 @@
     ///Constructor initializing with the current time values of the process
     TimeStamp(void *) { stamp();}
   
-    ///
+    ///\e
     TimeStamp &operator+=(const TimeStamp &b)
     {
       ts.tms_utime+=b.ts.tms_utime;
@@ -81,13 +81,13 @@
       real_time+=b.real_time;
       return *this;
     }
-    ///
+    ///\e
     TimeStamp operator+(const TimeStamp &b) const
     {
       TimeStamp t(*this);
       return t+=b;
     }
-    ///
+    ///\e
     TimeStamp &operator-=(const TimeStamp &b)
     {
       ts.tms_utime-=b.ts.tms_utime;
@@ -97,13 +97,12 @@
       real_time-=b.real_time;
       return *this;
     }
-    ///
+    ///\e
     TimeStamp operator-(const TimeStamp &b) const
     {
       TimeStamp t(*this);
       return t-=b;
     }
-
     ///The time ellapsed since the last call of stamp()
     TimeStamp ellapsed() const
     {
@@ -180,7 +179,7 @@
     ///This conversion computes the ellapsed time
     ///since the construction of \c t or since
     ///the last \c t.reset().
-    operator TimeStamp ()
+    operator TimeStamp () const
     {
       TimeStamp t;
       t.stamp();
@@ -194,6 +193,34 @@
       _reset();
       return start_time-t;
     }
+
+
+    ///Gives back the ellapsed user time of the process
+    double getUserTime() const
+    {
+      return operator TimeStamp().getUserTime();
+    }
+    ///Gives back the ellapsed system time of the process
+    double getSystemTime() const
+    {
+      return operator TimeStamp().getSystemTime();
+    }
+    ///Gives back the ellapsed user time of the process' children
+    double getCUserTime() const
+    {
+      return operator TimeStamp().getCUserTime();
+    }
+    ///Gives back the ellapsed user time of the process' children
+    double getCSystemTime() const
+    {
+      return operator TimeStamp().getCSystemTime();
+    }
+    ///Gives back the ellapsed real time of the process
+    double getRealTime() const
+    {
+      return operator TimeStamp().getRealTime();
+    }
+
   };
 
   ///Prints the time counters