function doZoom(size)
{
    document.getElementById('zoom').style.fontSize=size+'px';
}

function doPrint()
{
    window.print();
}