Function text

lib/web/renderjson.js:78–78

(txt)

                                  return true; }
    var stripQuotes = function(txt) { if (txt.startsWith("\"") && txt.endsWith("\"")) return txt.substring(1, txt.length-1); else return txt;}
    var text = function(txt) { return document.createTextNode(stripQuotes(txt)) };
    var div = function() { return document.createElement("div") };
    var span = function(classname) { var s = document.createElement("span");
                                     if (classname) s.className = classname;