X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=068b30d708cfb0efb319a900887a10a009f66834;hb=e499c2e36d8a39c4749b8e0e34438b49532d15b8;hp=30c138385e33b659b9c5f323273f7e79a8a2d8f7;hpb=11a20b624a4b5ed18008678cf6cd46dd9a32634d;p=helm.git diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index 30c138385..068b30d70 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,18 +642,19 @@ function advOneStep(xml) { disambcell.appendChild(okbutton); disambcell.appendChild(cancelbutton); - disable_toparea(); - matita.disambMode = true; updateSide(); throw "Stop"; } else if (is_defined(disamberr)) { - set_cps(disamberr.childNodes); - matita.unlockedbackup = unlocked.innerHTML.html_to_matita(); - matita.disambMode = true; - disable_toparea(); - next_cp(0); + // 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"; } else { @@ -703,12 +704,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 +719,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 +764,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")); } @@ -813,8 +818,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); @@ -871,6 +881,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 +957,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"; + } + else if (is_defined(localized)) { + unlocked.innerHTML = localized.childNodes[0].wholeText; } - if (is_defined(generic_err)) { - debug("Unmanaged error:\n" ^ generic_err.wholeText); + else if (is_defined(generic_err)) { + debug("Unmanaged error:\n" ^ generic_err.childNodes[0].wholeText); } } else { debug("goto bottom failed"); @@ -1076,10 +1096,8 @@ function retract() } resume(); }; - debug("retract 1"); pause(); callServer("retract",processor); - debug("retract 2"); } function openFile() @@ -1103,6 +1121,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 +1141,7 @@ function retrieveFile(thefile) debug("file open failed"); } }; - abortDialog(); + abortDialog("dialogBox"); callServer("open",processor,"file=" + escape(thefile)); } @@ -1174,26 +1195,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 +1228,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 +1240,7 @@ function saveDialog() function newDialog() { callback = function (fname) { - abortDialog(); + abortDialog("dialogBox"); saveFile(fname,"","",false,newDialog,true); }; showLibrary("Create new file", callback, newDialog); @@ -1263,7 +1286,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 +1315,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 +1331,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 +1382,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 +1454,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 +1575,9 @@ function resume() // retractButton.disabled = false; // cursorButton.disabled = false; // bottomButton.disabled = false; - enable_toparea(); - enable_editing(); + if (!matita.disambMode) { + enable_toparea(); + enable_editing(); + } }