// textsize.js
// simple javascript to resize (and remember) text size alterations made by user

function set_cookie(fontsize) 
{ 
var the_cookie = "textsize=" + fontsize; 
var the_date = new Date("December 31, 2050"); 
var the_cookie_date = the_date.toGMTString(); 
the_cookie = the_cookie + ";expires=" + the_cookie_date; 
document.cookie = the_cookie; 
} 

function read_cookie() 
{ 
var textsize = ''; 
var cookieInfo = document.cookie; 
var cookieInfoArray = cookieInfo.split("="); 
textsize = parseInt(cookieInfoArray[1]); 
return textsize; 
} 

function get_fontsize() 
{ 
var textsize = read_cookie(); 
if (textsize > 0){
}
else
{
textsize = 1;
}


set_cookie(textsize); 
} 

function change_size(val) 
{
} 

function change_and_set(val) 
{ 
change_size(val); 
set_cookie(val); 
}