function $$(el)
 {
  return document.getElementById(el);
 }