/* $Id: system.js 222 2005-07-06 20:51:57Z scottw $ 

   System-required javascript functions. */

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("editcontent");
  editbox.style.fontSize = "10pt";

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

  up.onclick = function () {
      editbox.style.fontSize = (parseFloat(editbox.style.fontSize) + 1).toString() + "pt";
      document.cookie = "editor-fontsize="+editbox.style.fontSize+"; expires="+later.toString();
    return false;
  };
  down.onclick = function () {
      editbox.style.fontSize = (parseFloat(editbox.style.fontSize) - 1).toString() + "pt";
      document.cookie = "editor-fontsize="+editbox.style.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());
}