1 files changed, 8 insertions, 3 deletions
diff --git a/lib/js/urweb.js b/lib/js/urweb.js
index 1cfbf0ca..fab15f35 100644
--- a/lib/js/urweb.js
+++ b/lib/js/urweb.js
@@ -136,6 +136,11 @@ function addSeconds(tm, n) {
     return tm + n * 1000000;
 }
 
+function stringToTime(string){
+   return  Date.parse(string)  // returns milliseconds and we need microseconds
+                      * 1000;
+}
+
 
 // Error handling
 
@@ -500,7 +505,7 @@ function normalizeTable(table) {
     var tbody = document.createElement("tbody");
     for (script = table.firstChild; script; script = next) {
         next = script.nextSibling;
-        
+
         tbody.insertBefore(script, tbody.firstChild);
     }
     table.appendChild(tbody);
@@ -1353,7 +1358,7 @@ function exec1(env, stack, e) {
             { var savedStack = stack.next, savedEnv = env;
                 e = {c: "c", v: function(v) { return exec1(savedEnv, savedStack, {c: "c", v: v}); } };}
             usedK = true;
-            break;      
+            break;
         default:
             whine("Unknown Ur expression kind " + e.c);
         }
@@ -1415,5 +1420,5 @@ function fresh() {
     return (--nextId).toString();
 }
 
-// App-specific code
 
+// App-specific code