From 3ce46320ae1c1af4731f176442bce4ac0243065d Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Wed, 28 Sep 2011 15:52:34 -0400
Subject: [PATCH] Include millisecond timings with commas.

---
 collects/meta/drdr/static/chart.js | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

diff --git a/collects/meta/drdr/static/chart.js b/collects/meta/drdr/static/chart.js
index 3677135c0c..c69c640a26 100644
--- a/collects/meta/drdr/static/chart.js
+++ b/collects/meta/drdr/static/chart.js
@@ -25,13 +25,26 @@ var options = { selection: { mode: "xy" },
                 grid: { clickable: true, hoverable : true }
               };
 
+function addCommas(nStr) {
+    var rgx = /(\d+)(\d{3})/;
+    while (rgx.test(nStr)) {
+        nStr = nStr.replace(rgx, '$1' + ',' + '$2');
+    }
+    return nStr;
+}
+
+// Number -> String
+function format_ms(ms) {
+    return addCommas(String(ms)) + " ms"
+}
+
 // Number -> String
 function format_time(ms) {
     if (ms >= 300000)
-        return Number(ms/60000).toFixed(2) + " m"
+        return Number(ms/60000).toFixed(2) + " m " + "("+ format_ms(ms)+")";
     if (ms >= 10000)
-        return Number(ms/1000).toFixed(2) + " s"
-    return String(ms) + " ms";
+        return Number(ms/1000).toFixed(2) + " s" + "("+ format_ms(ms)+")";
+    return format_ms(ms);
 }
 
 function legend_click(l) {