improvements to date formatting

- leading zeros on month/day
- milliseconds in chat tooltips

code/chat.js

@@ -394,7 +394,10 @@ window.chat.renderDivider = function(text) {
 
 window.chat.renderMsg = function(msg, nick, time, team, msgToPlayer, systemNarrowcast) {
   var ta = unixTimeToHHmm(time);
-  var tb = unixTimeToString(time, true);
+  var tb = unixTimeToDateTimeString(time, true);
+  //add <small> tags around the milliseconds
+  tb = (tb.slice(0,19)+'<small class="milliseconds">'+tb.slice(19)+'</small>').replace(/</g,'&lt;').replace(/>/g,'&gt;').replace(/"/g,'&quot;');
+
   // help cursor via “#chat time”
   var t = '<time title="'+tb+'" data-timestamp="'+time+'">'+ta+'</time>';
   if ( msgToPlayer )

code/portal_detail_display.js

@@ -27,7 +27,7 @@ window.renderPortalDetails = function(guid) {
   var playerText = player ? ['owner', player] : null;
 
   var time = d.captured
-    ? '<span title="' + unixTimeToString(d.captured.capturedTime, true) + '">'
+    ? '<span title="' + unixTimeToDateTimeString(d.captured.capturedTime, false) + '">'
       +  unixTimeToString(d.captured.capturedTime) + '</span>'
     : null;
   var sinceText  = time ? ['since', time] : null;

code/utils_misc.js

@@ -124,13 +124,20 @@ window.postAjax = function(action, data, success, error) {
   return result;
 }
 
-// converts unix timestamps to HH:mm:ss format if it was today;
+window.zeroPad = function(number,pad) {
+  number = number.toString();
+  var zeros = pad - number.length;
+  return Array(zeros>0?zeros+1:0).join("0") + number;
+}
+
+
+// converts javascript timestamps to HH:mm:ss format if it was today;
 // otherwise it returns YYYY-MM-DD
 window.unixTimeToString = function(time, full) {
   if(!time) return null;
   var d = new Date(typeof time === 'string' ? parseInt(time) : time);
   var time = d.toLocaleTimeString();
-  var date = d.getFullYear()+'-'+(d.getMonth()+1)+'-'+d.getDate();
+  var date = d.getFullYear()+'-'+zeroPad(d.getMonth()+1,2)+'-'+zeroPad(d.getDate(),2);
   if(typeof full !== 'undefined' && full) return date + ' ' + time;
   if(d.toDateString() == new Date().toDateString())
     return time;
@@ -138,6 +145,15 @@ window.unixTimeToString = function(time, full) {
     return date;
 }
 
+// converts a javascript time to a precise date and time (optionally with millisecond precision)
+// formatted in ISO-style YYYY-MM-DD hh:mm:ss.mmm - but using local timezone
+window.unixTimeToDateTimeString = function(time, millisecond) {
+  if(!time) return null;
+  var d = new Date(typeof time === 'string' ? parseInt(time) : time);
+  return d.getFullYear()+'-'+zeroPad(d.getMonth()+1,2)+'-'+zeroPad(d.getDate(),2)
+    +' '+d.toLocaleTimeString()+(millisecond?'.'+zeroPad(d.getMilliseconds(),3):'');
+}
+
 window.unixTimeToHHmm = function(time) {
   if(!time) return null;
   var d = new Date(typeof time === 'string' ? parseInt(time) : time);