
function toggle_toc()
{
	var link = document.getElementById( "toc-link" );
	var data = document.getElementById( "toc-data" );
	if ( link.innerHTML == "[Show]" )
	{
		link.innerHTML = "[Hide]";
		data.style.display = "block";
	}
	else
	{
		link.innerHTML = "[Show]";
		data.style.display = "none";
	}	
}


