document.ondblclick = function () {
	var file = location.href;
	file = file.replace("http://127.0.0.1", "file:///F:");
	file = file.replace(/[?#].+/, "");
	if (file.charAt(file.length -1) == "/") {
		try {
			file += document.getElementsByName("filename")[0].content;
		} catch(e) {
			file += "index.html";
		}
	}
	location.href = "view-source:" + file;
}