X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=cd25cd15a68b2e349647378de40deb9551c338df;hb=0e16720654c6667b94433e91dddc3c53b904e200;hp=30c138385e33b659b9c5f323273f7e79a8a2d8f7;hpb=928af763320668168206e88d93e8a77698f3b925;p=helm.git diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index 30c138385..cd25cd15a 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -220,7 +220,7 @@ function strip_tags(tagname,classname) tags[i].parentNode.insertBefore(children[j],tags[i]); } } - while (tags.length > 0) { + for (var i = 0;tags.length > i;i++) { tags[0].parentNode.removeChild(tags[0]); } } @@ -582,7 +582,7 @@ function advOneStep(xml) { // len1 = unlocked.innerHTML.length; // len2 = len0 - len1; var len2 = parsedtxt.length; - var metasenv = xml.getElementsByTagName("meta"); + metasenv = xml.getElementsByTagName("meta"); statements = listcons(len2,statements); unlocked.scrollIntoView(true); return len; @@ -642,19 +642,20 @@ function advOneStep(xml) { disambcell.appendChild(okbutton); disambcell.appendChild(cancelbutton); - disable_toparea(); - matita.disambMode = true; updateSide(); - throw "Stop"; + throw "Wait"; } else if (is_defined(disamberr)) { - set_cps(disamberr.childNodes); - matita.unlockedbackup = unlocked.innerHTML.html_to_matita(); - matita.disambMode = true; - disable_toparea(); - next_cp(0); - throw "Stop"; + // must be fixed in a daemon: it makes sense to return a + // disambiguation error with no choices + if (disamberr.childNodes.length > 0) { + set_cps(disamberr.childNodes); + matita.unlockedbackup = unlocked.innerHTML.html_to_matita(); + matita.disambMode = true; + next_cp(0); + } + throw "Wait"; } else { var error = xml.getElementsByTagName("error")[0]; @@ -677,9 +678,11 @@ function advanceForm1() debug("advance failed"); } } catch (e) { - // nothing to do + if (e == "Stop") + resume(); + else + pause(); }; - resume(); }; pause(); callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape()); @@ -703,12 +706,12 @@ function get_choice_opts(i) { var href = choices[j].getAttribute("href"); var title = choices[j].getAttribute("title"); var desc; - if (is_defined(title)) { + if (is_defined(title) && title != null) { desc = title; - } else if (is_defined(href)) { + } else if (is_defined(href) && href != null) { desc = href; } else { - desc = "Preliminary error"; + desc = null; } res[j] = document.createElement("input"); @@ -718,7 +721,7 @@ function get_choice_opts(i) { res[j].setAttribute("choiceno",j); res[j].setAttribute("href",href); res[j].setAttribute("title",title); - res[j].setAttribute("desc",desc); + if (desc != null) res[j].setAttribute("desc",desc); if (j == 0) res[j].setAttribute("checked",""); } @@ -763,15 +766,19 @@ function next_cp(curcp) { var mid = unlockedtxt.substring(start,stop).matita_to_html(); var post = unlockedtxt.substring(stop).matita_to_html(); unlocked.innerHTML = pre + - "" + + "" + mid + "" + post; - var title = "

Disambiguation failed

"; + var title = "

Error diagnostics

"; disambcell.innerHTML = title; var choices = get_choice_opts(curcp); for (var i = 0;i < choices.length;i++) { disambcell.appendChild(choices[i]); - disambcell.appendChild(document.createTextNode(choices[i].getAttribute("desc"))); + var desc = choices[i].getAttribute("desc"); + if (!is_defined(desc) || desc == null) { + desc = "Interpretation " + i; + } + disambcell.appendChild(document.createTextNode(desc)); disambcell.appendChild(document.createElement("br")); } @@ -789,7 +796,7 @@ function next_cp(curcp) { var tryagainbutton = document.createElement("input"); tryagainbutton.setAttribute("type","button"); if (new_curcp > 0) { - tryagainbutton.setAttribute("value","Try something else"); + tryagainbutton.setAttribute("value","None of the above"); } else { tryagainbutton.setAttribute("value","Restart"); } @@ -813,8 +820,13 @@ function show_failures() { var choiceno = parseInt(choice.getAttribute("choiceno")); var choicedesc = choice.getAttribute("desc"); - var title = "

Disambiguation failed

"; - var subtitle = "

Errors at node " + cpno + " = " + choicedesc + "

"; + var title = "

Error diagnostics

"; + var subtitle; + if (is_defined(choicedesc) && choicedesc != null) { + subtitle = "

Errors at node " + cpno + " = " + choicedesc + "

"; + } else { + subtitle = "

Global errors:

"; + } disambcell.innerHTML = title + subtitle; var failures = get_failure_opts(cpno,choiceno); @@ -834,7 +846,7 @@ function show_failures() { cancelbutton.setAttribute("onclick","cancel_disambiguate()"); var backbutton = document.createElement("input"); backbutton.setAttribute("type","button"); - backbutton.setAttribute("value","<< Back"); + backbutton.setAttribute("value","<< Go back"); backbutton.setAttribute("onclick","next_cp(" + cpno + ")"); disambcell.appendChild(backbutton); @@ -871,6 +883,7 @@ function gotoBottom() var localized = xml.getElementsByTagName("localized")[0]; var ambiguity = xml.getElementsByTagName("ambiguity")[0]; var generic_err = xml.getElementsByTagName("error")[0]; + var disamberr = xml.getElementsByTagName("disamberror")[0]; for (var i = 0;i < parsed.length; i++) { var len = parsed[i].getAttribute("length"); // len0 = unlocked.innerHTML.length; @@ -946,16 +959,25 @@ function gotoBottom() disambcell.appendChild(okbutton); disambcell.appendChild(cancelbutton); - disable_toparea(); - matita.disambMode = true; updateSide(); } - if (is_defined(localized)) { - unlocked.innerHTML = localized.wholeText; + else if (is_defined(disamberr)) { + // must be fixed in a daemon: it makes sense to return a + // disambiguation error with no choices + if (disamberr.childNodes.length > 0) { + set_cps(disamberr.childNodes); + matita.unlockedbackup = unlocked.innerHTML.html_to_matita(); + matita.disambMode = true; + next_cp(0); + } + throw "Stop"; } - if (is_defined(generic_err)) { - debug("Unmanaged error:\n" ^ generic_err.wholeText); + else if (is_defined(localized)) { + unlocked.innerHTML = localized.childNodes[0].wholeText; + } + else if (is_defined(generic_err)) { + debug("Unmanaged error:\n" ^ generic_err.childNodes[0].wholeText); } } else { debug("goto bottom failed"); @@ -1036,7 +1058,11 @@ function gotoPos(offset) } catch (er) { init_autotraces(); populate_goalarray(metasenv); - resume(); + if (er == "Stop") + resume(); + else + pause(); + } } else { init_autotraces(); @@ -1076,10 +1102,8 @@ function retract() } resume(); }; - debug("retract 1"); pause(); callServer("retract",processor); - debug("retract 2"); } function openFile() @@ -1103,6 +1127,9 @@ function retrieveFile(thefile) { if (is_defined(xml)) { changeFile(thefile); + matita.disambMode = false; + matita.proofMode = false; + updateSide(); lockedbackup = "" locked.innerHTML = lockedbackup; // code originally used in google chrome (problems with mozilla) @@ -1120,7 +1147,7 @@ function retrieveFile(thefile) debug("file open failed"); } }; - abortDialog(); + abortDialog("dialogBox"); callServer("open",processor,"file=" + escape(thefile)); } @@ -1174,26 +1201,28 @@ function uploadDialog() function uploadOK() { var file = document.getElementById("uploadFilename").files[0]; - if (file) { - var filecontent = file.getAsText("UTF-8"); - locked.innerHTML = lockedbackup; - unlocked.innerHTML = filecontent; - uploadBox.style.display = "none"; - } // if (file) { -// var reader = new FileReader(); -// reader.readAsText(file, "UTF-8"); -// reader.onloadend = function (evt) { -// lockedbackup = ""; -// locked.innerHTML = lockedbackup -// unlocked.innerHTML = evt.target.result; -// uploadBox.style.display = "none"; -// } -// reader.onerror = function (evt) { -// debug("file open failed"); -// uploadBox.style.display = "none"; -// } +// var filecontent = file.getAsText("UTF-8"); +// locked.innerHTML = lockedbackup; +// unlocked.innerHTML = filecontent; +// uploadBox.style.display = "none"; // } + if (file) { + var reader = new FileReader(); + reader.onerror = function (evt) { + debug("file open failed"); + } + reader.onload = function (evt) { + lockedbackup = ""; + locked.innerHTML = lockedbackup; + unlocked.innerHTML = ""; + unlocked.appendChild(document.createTextNode(evt.target.result)); + uploadBox.style.display = "none"; + } + try { reader.readAsText(file, "UTF-8"); } + catch (err) { /* nothing to do */ }; + uploadBox.style.display = "none"; + } } function openDialog() @@ -1205,7 +1234,7 @@ function openDialog() function saveDialog() { callback = function (fname) { - abortDialog(); + abortDialog("dialogBox"); saveFile(fname, (locked.innerHTML.html_to_matita()).sescape(), (unlocked.innerHTML.html_to_matita()).sescape(), @@ -1217,7 +1246,7 @@ function saveDialog() function newDialog() { callback = function (fname) { - abortDialog(); + abortDialog("dialogBox"); saveFile(fname,"","",false,newDialog,true); }; showLibrary("Create new file", callback, newDialog); @@ -1263,7 +1292,7 @@ function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog,reloadFile) } function createDir() { - abortDialog(); + abortDialog("dialogBox"); dirname = prompt("New directory name:\ncic:/matita/","newdir"); if (dirname != null) { processor = function(xml) { @@ -1292,7 +1321,7 @@ function commitAll() alert("Commit executed: see details in the log.\n\n" + "NOTICE: this message does NOT imply (yet) that the commit was successful."); } else { - alert("Commit failed!"); + alert("Commit failed!\n(maybe you don't have permissionis to commit?)"); } resume(); }; @@ -1308,7 +1337,7 @@ function updateAll() "Details:\n" + xml.getElementsByTagName("details")[0].textContent); } else { - alert("Update failed!"); + alert("Update failed!\n(maybe you don't have permissions to update?)"); } resume(); }; @@ -1359,8 +1388,8 @@ function showDialog(title,content,callback) { } function abortDialog(dialog) { + document.getElementById(dialog).style.display = "none"; $('#mask').hide(); - dialogBox.style.display = "none"; } function removeElement(id) { @@ -1431,8 +1460,10 @@ function get_checked_index(name) { function cancel_disambiguate() { matita.disambMode = false; - enable_toparea(); - enable_editing(); + resume(); + // enable_toparea(); + // enable_editing(); + strip_tags("span","error"); updateSide(); } @@ -1550,7 +1581,9 @@ function resume() // retractButton.disabled = false; // cursorButton.disabled = false; // bottomButton.disabled = false; - enable_toparea(); - enable_editing(); + if (!matita.disambMode) { + enable_toparea(); + enable_editing(); + } }