From f46d60c6c12f12ccb911cbc628d0208f34584e4b Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Wed, 28 Sep 2011 11:01:08 -0400
Subject: [PATCH] Improve tooltip time printing.

---
 collects/meta/drdr/static/chart.js | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/collects/meta/drdr/static/chart.js b/collects/meta/drdr/static/chart.js
index a98a555f09..3677135c0c 100644
--- a/collects/meta/drdr/static/chart.js
+++ b/collects/meta/drdr/static/chart.js
@@ -25,6 +25,15 @@ var options = { selection: { mode: "xy" },
                 grid: { clickable: true, hoverable : true }
               };
 
+// Number -> String
+function format_time(ms) {
+    if (ms >= 300000)
+        return Number(ms/60000).toFixed(2) + " m"
+    if (ms >= 10000)
+        return Number(ms/1000).toFixed(2) + " s"
+    return String(ms) + " ms";
+}
+
 function legend_click(l) {
     show_hide[l] = !show_hide[l];
     show();
@@ -53,7 +62,7 @@ function makeTooltip(item,path) {
     showTooltip(item.pageX, item.pageY,
                 item.series.label + ' at <a href="http://drdr.racket-lang.org/'
                 + x + path + '">push ' + x + "</a>: "
-                + y + " ms");
+                + format_time(y));
 }
 placeholder.bind("plotselected", handle_selection);