diff lib/js/urweb.js @ 1620:43f22a8f76cc

Allow sources to be returned by RPCs
author Adam Chlipala <adam@chlipala.net>
date Sat, 03 Dec 2011 10:00:10 -0500
parents 15e0c935c91b
children 62d6d452c2b8
line wrap: on
line diff
--- a/lib/js/urweb.js	Sat Dec 03 09:44:07 2011 -0500
+++ b/lib/js/urweb.js	Sat Dec 03 10:00:10 2011 -0500
@@ -976,6 +976,10 @@
         return null;
 }
 
+function parseSource(s1, s2) {
+    return eval("s" + s1 + "_" + s2);
+}
+
 function uf(s) {
     if (s.length == 0)
         return "_";