// Atree specific javascript

// cookie names
var fontCookie = "CrunchFontSize";

// font size defaults
var default_font_size = 14;
var min_font_size = 6;
var max_font_size = 72;

// changes the document font size by altering the font size attribute
// of the tag body, fs assumed to be in the form **px where ** is a two digit number
function setBodyFontSize(fs)
{
	document.body.style.fontSize = fs;
	setCookie(fontCookie,fs,365);
}

function increaseFontSize()
{
	var curr_size = document.body.style.fontSize;
	if(curr_size != max_font_size.toString() + "px")
	{
		var n = parseInt(curr_size.substr(0,curr_size.length-2));
		n = n + 2;
		setBodyFontSize(n.toString() + "px");
	}
}

function decreaseFontSize()
{
	var curr_size = document.body.style.fontSize;
	if(curr_size != min_font_size.toString() + "px")
	{
		var n = parseInt(curr_size.substr(0,curr_size.length-2));
		n = n - 2;
		setBodyFontSize(n.toString() + "px");
	}
}

// used to check for a cookie when the page loads
function checkCookie()
{
	var font_size = getCookie(fontCookie);
	if(font_size == null)
		font_size = default_font_size.toString() + "px";
	setBodyFontSize(font_size);
}

window.onload = function(e) {
	checkCookie();
}