function open_blank(url) {
    // Generate a window name from the URL and open it in a new window.
    window.open(url,url.replace(/[^\w]/g,"_"),"location=yes,menubar=yes,resizable=yes,status=yes,toolbar=yes");
}