# HG changeset patch
# User wenzelm
# Date 870793391 -7200
# Node ID fb25f00d1c70dfccc8ea51e76e13a74eee917991
# Parent  193cc37e6f6004fbc3878d47f9608337b10d1a6b
cleaned up;
added getenv;

diff -r 193cc37e6f60 -r fb25f00d1c70 src/Pure/ML-Systems/smlnj-0.93.ML
--- a/src/Pure/ML-Systems/smlnj-0.93.ML	Tue Aug 05 17:02:50 1997 +0200
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Tue Aug 05 17:03:11 1997 +0200
@@ -30,29 +30,34 @@
 (* timing *)
 
 local
-  (*print microseconds, suppressing trailing zeroes*)
-  fun umakestring 0 = ""
-    | umakestring n =
-        chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000));
+
+(*print microseconds, suppressing trailing zeroes*)
+fun umakestring 0 = ""
+  | umakestring n =
+      chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000));
+
 in
-  (*a conditional timing function: applies f to () and, if the flag is true,
-    prints its runtime*)
-  fun cond_timeit flag f =
-    if flag then
-      let fun string_of_time (System.Timer.TIME {sec, usec}) =
-              makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
-          open System.Timer;
-          val start = start_timer()
-          val result = f();
-          val nongc = check_timer(start)
-          and gc = check_timer_gc(start);
-          val both = add_time(nongc, gc)
-      in  print("Non GC " ^ string_of_time nongc ^
-                 "   GC " ^ string_of_time gc ^
-                 "  both "^ string_of_time both ^ " secs\n");
-          result
-      end
-    else f();
+
+(*a conditional timing function: applies f to () and, if the flag is true,
+  prints its runtime*)
+
+fun cond_timeit flag f =
+  if flag then
+    let fun string_of_time (System.Timer.TIME {sec, usec}) =
+            makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
+        open System.Timer;
+        val start = start_timer()
+        val result = f();
+        val nongc = check_timer(start)
+        and gc = check_timer_gc(start);
+        val both = add_time(nongc, gc)
+    in  print("Non GC " ^ string_of_time nongc ^
+               "   GC " ^ string_of_time gc ^
+               "  both "^ string_of_time both ^ " secs\n");
+        result
+    end
+  else f();
+
 end;