# HG changeset patch
# User wenzelm
# Date 1330769357 -3600
# Node ID 46acd255810d0fb2cb5a0f7375965a8e6869d354
# Parent  807a5d219c239dcc610a6d11b9d71127f93bc42e
relevant timing as in ML;
more PIDE modules;

diff -r 807a5d219c23 -r 46acd255810d src/Pure/General/time.scala
--- a/src/Pure/General/time.scala	Fri Mar 02 21:45:45 2012 +0100
+++ b/src/Pure/General/time.scala	Sat Mar 03 11:09:17 2012 +0100
@@ -21,8 +21,11 @@
   def min(t: Time): Time = if (ms < t.ms) this else t
   def max(t: Time): Time = if (ms > t.ms) this else t
 
+  def is_relevant: Boolean = ms >= 1
+
   override def toString =
     String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
+
   def message: String = toString + "s"
 }
 
diff -r 807a5d219c23 -r 46acd255810d src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Fri Mar 02 21:45:45 2012 +0100
+++ b/src/Pure/General/timing.scala	Sat Mar 03 11:09:17 2012 +0100
@@ -1,4 +1,5 @@
 /*  Title:      Pure/General/timing.scala
+    Module:     PIDE
     Author:     Makarius
 
 Basic support for time measurement.
@@ -14,17 +15,24 @@
     val start = java.lang.System.currentTimeMillis()
     val result = Exn.capture(e)
     val stop = java.lang.System.currentTimeMillis()
-    java.lang.System.err.println(
-      (if (message == null || message.isEmpty) "" else message + ": ") +
-        Time.ms(stop - start).message + " elapsed time")
+
+    val timing = Time.ms(stop - start)
+    if (timing.is_relevant)
+      java.lang.System.err.println(
+        (if (message == null || message.isEmpty) "" else message + ": ") +
+          timing.message + " elapsed time")
+
     Exn.release(result)
   }
 }
 
 class Timing(val elapsed: Time, val cpu: Time, val gc: Time)
 {
+  def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant
+
   def message: String =
     elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
+
   override def toString = message
 }