function $(id){ return document.getElementById(id) }
function encode_entities(s){
  var result = '';
  for (var i = 0; i < s.length; i++){    var c = s.charAt(i);    result += {'<':'&#60;', '>':'&#62;', '&':'&#38;', '\"':'&#34;', '\'':'&#39;', '-':'&#45;', '/':'&#47;', '=':'&#61;', '!':'&#33;', '(':'&#40;', ')':'&#41;', '[':'&#91;', ']':'&#93;', '{':'&#123;', '}':'&#125;', '\n':'&#13;'}[c] || c;  }  return result;}
function do_encode(e){  $('pre').innerHTML = $('dst').value = encode_entities(e.value)}