comparison 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
comparison
equal deleted inserted replaced
1619:15e0c935c91b 1620:43f22a8f76cc
974 return r; 974 return r;
975 else 975 else
976 return null; 976 return null;
977 } 977 }
978 978
979 function parseSource(s1, s2) {
980 return eval("s" + s1 + "_" + s2);
981 }
982
979 function uf(s) { 983 function uf(s) {
980 if (s.length == 0) 984 if (s.length == 0)
981 return "_"; 985 return "_";
982 s = s.replace(new RegExp ("\\.", "g"), ".2E"); 986 s = s.replace(new RegExp ("\\.", "g"), ".2E");
983 return (s.charAt(0) == '_' ? "_" : "") + encodeURIComponent(s).replace(new RegExp ("%", "g"), "."); 987 return (s.charAt(0) == '_' ? "_" : "") + encodeURIComponent(s).replace(new RegExp ("%", "g"), ".");