function tex_img(name, dpi) {
  if (dpi == undefined) dpi = 100;
  tex = escape(document.getElementById(name).text);
  url = "http://blush.ee.columbia.edu/adam/tex2gif.cgi?dpi="+dpi+"&tex="+tex;
  document.write("<img style=vertical-align:middle src=\""+url+"\">");
}
function math_img(math, dpi) {
  if (dpi == undefined) dpi = 100;
  head = "\\documentclass[12pt]{article}\n\\pagestyle{empty}\n\\begin{document}\n\\begin{displaymath}\n";
  foot = "\n\\end{displaymath}\n\\end{document}";
  tex = escape(head+math+foot);
  url = "http://blush.ee.columbia.edu/adam/tex2gif.cgi?dpi="+dpi+"&tex="+tex;
  document.write("<img style=vertical-align:middle src=\""+url+"\">");
}
function dot_img(name, dpi) {
  if (dpi == undefined) dpi = 100;
  dot = document.getElementById(name).text;
  dot = escape(dot.replace(/\n\s*/g, "\n"));
  // doesn't exist yet...!
  url = "http://blush.ee.columbia.edu/adam/dot2gif.cgi?dpi="+dpi+"&tex="+tex;
  document.write("<img src=\""+url+"\">");
}