X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=221ef90b56f3c6361d5338d48c71d5a89548498e;hb=5f1afbcf716a9275f70baa02a5a464bd2abc0726;hp=c0b9458425ccde715e620507f978bb74b9de3b1b;hpb=0cda74283ace2af53332667a32978dac2701dc78;p=helm.git diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index c0b945842..221ef90b5 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -644,7 +644,7 @@ function retrieveFile(thefile) callServer("open",processor,"file=" + escape(thefile)); } -function showLibrary() +function showLibrary(title,callback) { var req = null; // pause(); @@ -675,7 +675,7 @@ function showLibrary() if(stat == 200) { debug(req.responseText); - showDialog("

Library

",req.responseText); + showDialog("

" + title + "

",req.responseText, callback); } } }; @@ -685,21 +685,44 @@ function showLibrary() } -function saveFile() +function openDialog() +{ + callback = function (fname) { retrieveFile(fname); }; + showLibrary("Open file", callback); +} + +function saveDialog() +{ + callback = function (fname) { saveFile(fname,false); }; + showLibrary("Save file as", callback); +} + +function saveFile(fname,force) { + if (!is_defined(fname) { + fname = current_fname; + } processor = function(xml) { if (is_defined(xml)) { + if (xml.childNodes[0].textContent != "ok") { + if (confirm("File already exists. Do you want to proceed anyway?")) { + saveFile(fname,true); + } else { + saveDialog(); + } + } else debug("file saved!"); } else { debug("save file failed"); } resume(); }; - if (is_defined(current_fname)) { + if (is_defined(fname)) { pause(); - callServer("save",processor,"file=" + escape(current_fname) + + callServer("save",processor,"file=" + escape(fname) + "&locked=" + (locked.innerHTML.html_to_matita()).sescape() + - "&unlocked=" + (unlocked.innerHTML.html_to_matita()).sescape()); + "&unlocked=" + (unlocked.innerHTML.html_to_matita()).sescape() + + "&force=" + force); } else { debug("no file selected"); } } @@ -730,10 +753,11 @@ function showSequent() { workarea.appendChild(goalcell); } -function showDialog(title,content) { +function showDialog(title,content,callback) { dialogTitle.innerHTML = title; dialogContent.innerHTML = content; dialogBox.style.display = "block"; + dialogBox.callback = callback; } function removeElement(id) {