var footWidth = "50%";

function foot(e,text) {
    l=document.getElementById('float');
    l.innerHTML=text;
    l.style.position = 'absolute';
    l.style.left = e.clientX + 5;
    l.style.top= e.offsetY + 100;
    l.style.width = footWidth;
    l.style.visibility='visible';
    l.style.display='block';
}

function editor_fontsize() {
  document.write("<div id=PumaCodeControls>" +
                 "  Editor font size: <button id=font_up title='Increase font size'>bigger</button> "+
                 "<button id=font_down title='Decrease font size'>smaller</button> <!-- button id=showcookies>(@)</button -->"+
                 "</div>");
  var up = document.getElementById("font_up");
  var down = document.getElementById("font_down");
  var cookies = document.getElementById("showcookies");
  var editbox = document.getElementById("editor");
  editbox.style.fontSize = "10pt";

  var now = new Date();
  var later = new Date(now.getTime() + 1000 * 60 * 60 * 24 * 360);

  up.onclick = function () {
    with (editbox.style) {
      fontSize = (parseFloat(fontSize) + 1).toString() + "pt";
      document.cookie = "editor-fontsize="+fontSize+"; expires="+later.toString();
    }
    return false;
  };
  down.onclick = function () {
    with (editbox.style) {
      fontSize = (parseFloat(fontSize) - 1).toString() + "pt";
      document.cookie = "editor-fontsize="+fontSize+"; expires="+later.toString();
    }
    return false;
  };
}

var days = new Array('Sunday', 'Monday', 'Tuesday',
                         'Wednesday', 'Thursday', 'Friday',
                         'Saturday');
var months = new Array('January', 'February', 'March',
                           'April', 'May', 'June', 'July',
                           'August', 'September', 'October',
                           'November', 'December');
var date = new Date();

function print_time() {
  document.write(days[date.getDay()] + ', ' +
                 months[date.getMonth()] + ' ' +
                 date.getDate() + ', ' +
                 date.getFullYear());
}