1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/framework/env/encode/json.lua	Sun Oct 25 12:00:00 2009 +0100
     1.3 @@ -0,0 +1,34 @@
     1.4 +--[[--
     1.5 +json_string =  -- JavaScript code representing the given datum (with quotes, if needed)
     1.6 +encode.json(
     1.7 +  obj          -- true, false, nil or a number or string
     1.8 +)
     1.9 +
    1.10 +This function encodes any native datatype or atom in JavaScript object notation (JSON).
    1.11 +
    1.12 +--]]--
    1.13 +
    1.14 +function encode.json(obj)
    1.15 +  if obj == nil then
    1.16 +    return "null";
    1.17 +  elseif atom.has_type(obj, atom.boolean) then
    1.18 +    return tostring(obj)
    1.19 +  elseif atom.has_type(obj, atom.number) then
    1.20 +    return tostring(obj)
    1.21 +  else
    1.22 +    return
    1.23 +      "'" ..
    1.24 +      string.gsub(atom.dump(obj), ".",
    1.25 +        function (char)
    1.26 +          if char == "\r" then return "\\r"  end
    1.27 +          if char == "\n" then return "\\n"  end
    1.28 +          if char == "\\" then return "\\\\" end
    1.29 +          if char == "'"  then return "\\'"  end
    1.30 +          if char == "/"  then return "\\/"  end  -- allowed according to RFC4627, needed for </script>
    1.31 +          local byte = string.byte(char)
    1.32 +          if byte < 32 then return string.format("\\u%04x", byte) end
    1.33 +        end
    1.34 +      ) ..
    1.35 +      "'"
    1.36 +  end
    1.37 +end