var STRING_SUBSTITUTIONS = {    // table of character substitutions
  '\t': '\\t',
  '\r': '\\r',
  '\n': '\\n',
  '"' : '\\"',
  '\\': '\\\\'
};