X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;fp=matitaB%2Fmatita%2Fmatitaweb.js;h=30c138385e33b659b9c5f323273f7e79a8a2d8f7;hb=928af763320668168206e88d93e8a77698f3b925;hp=23bf4d396c62acba6d861c1d96485fa381e7109f;hpb=c9c6cae5121a25b05450ea42578f14f74569cfbf;p=helm.git diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index 23bf4d396..30c138385 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -564,109 +564,122 @@ function callServer(servicename,processResponse,reqbody) } -function advanceForm1() -{ - processor = function(xml) { - if (is_defined(xml)) { - var parsed = xml.getElementsByTagName("parsed")[0]; - var ambiguity = xml.getElementsByTagName("ambiguity")[0]; - var disamberr = xml.getElementsByTagName("disamberror")[0]; - if (is_defined(parsed)) { - // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND"); - var len = parseInt(parsed.getAttribute("length")); - // len0 = unlocked.innerHTML.length; - var unescaped = unlocked.innerHTML.html_to_matita(); - var parsedtxt = parsed.childNodes[0].wholeText; - //parsedtxt = unescaped.substr(0,len); - var unparsedtxt = unescaped.substr(len); - lockedbackup += parsedtxt; - locked.innerHTML = lockedbackup; - unlocked.innerHTML = unparsedtxt.matita_to_html(); - // len1 = unlocked.innerHTML.length; - // len2 = len0 - len1; - var len2 = parsedtxt.length; - var metasenv = xml.getElementsByTagName("meta"); - populate_goalarray(metasenv); - init_autotraces(); - statements = listcons(len2,statements); - unlocked.scrollIntoView(true); - } - else if (is_defined(ambiguity)) { - var start = parseInt(ambiguity.getAttribute("start")); - var stop = parseInt(ambiguity.getAttribute("stop")); - var choices = xml.getElementsByTagName("choice"); - - matita.ambiguityStart = start; - matita.ambiguityStop = stop; - matita.unlockedbackup = unlocked.innerHTML.html_to_matita(); - matita.interpretations = []; - - var unlockedtxt = unlocked.innerHTML.html_to_matita(); - var pre = unlockedtxt.substring(0,start).matita_to_html(); - var mid = unlockedtxt.substring(start,stop).matita_to_html(); - var post = unlockedtxt.substring(stop).matita_to_html(); - unlocked.innerHTML = pre + - "" + - mid + "" + post; - - var title = "

Ambiguous input

"; - disambcell.innerHTML = title; - for (i = 0;i < choices.length;i++) { - matita.interpretations[i] = new Object(); +function advOneStep(xml) { + var parsed = xml.getElementsByTagName("parsed")[0]; + var ambiguity = xml.getElementsByTagName("ambiguity")[0]; + var disamberr = xml.getElementsByTagName("disamberror")[0]; + if (is_defined(parsed)) { + // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND"); + var len = parseInt(parsed.getAttribute("length")); + // len0 = unlocked.innerHTML.length; + var unescaped = unlocked.innerHTML.html_to_matita(); + var parsedtxt = parsed.childNodes[0].wholeText; + //parsedtxt = unescaped.substr(0,len); + var unparsedtxt = unescaped.substr(len); + lockedbackup += parsedtxt; + locked.innerHTML = lockedbackup; + unlocked.innerHTML = unparsedtxt.matita_to_html(); + // len1 = unlocked.innerHTML.length; + // len2 = len0 - len1; + var len2 = parsedtxt.length; + var metasenv = xml.getElementsByTagName("meta"); + statements = listcons(len2,statements); + unlocked.scrollIntoView(true); + return len; + } + else if (is_defined(ambiguity)) { + var start = parseInt(ambiguity.getAttribute("start")); + var stop = parseInt(ambiguity.getAttribute("stop")); + var choices = xml.getElementsByTagName("choice"); + + matita.ambiguityStart = start; + matita.ambiguityStop = stop; + matita.unlockedbackup = unlocked.innerHTML.html_to_matita(); + matita.interpretations = []; + + var unlockedtxt = unlocked.innerHTML.html_to_matita(); + var pre = unlockedtxt.substring(0,start).matita_to_html(); + var mid = unlockedtxt.substring(start,stop).matita_to_html(); + var post = unlockedtxt.substring(stop).matita_to_html(); + unlocked.innerHTML = pre + + "" + + mid + "" + post; + + var title = "

Ambiguous input

"; + disambcell.innerHTML = title; + for (i = 0;i < choices.length;i++) { + matita.interpretations[i] = new Object(); + + var href = choices[i].getAttribute("href"); + var title = choices[i].getAttribute("title"); + var desc = choices[i].childNodes[0].nodeValue; + + matita.interpretations[i].href = href; + matita.interpretations[i].title = title; + matita.interpretations[i].desc = desc; + + var choice = document.createElement("input"); + choice.setAttribute("type","radio"); + choice.setAttribute("name","interpr"); + choice.setAttribute("href",href); + choice.setAttribute("title",title); + if (i == 0) choice.setAttribute("checked",""); + + disambcell.appendChild(choice); + disambcell.appendChild(document.createTextNode(desc)); + disambcell.appendChild(document.createElement("br")); + } - var href = choices[i].getAttribute("href"); - var title = choices[i].getAttribute("title"); - var desc = choices[i].childNodes[0].nodeValue; + var okbutton = document.createElement("input"); + okbutton.setAttribute("type","button"); + okbutton.setAttribute("value","OK"); + okbutton.setAttribute("onclick","do_disambiguate()"); + var cancelbutton = document.createElement("input"); + cancelbutton.setAttribute("type","button"); + cancelbutton.setAttribute("value","Cancel"); + cancelbutton.setAttribute("onclick","cancel_disambiguate()"); - matita.interpretations[i].href = href; - matita.interpretations[i].title = title; - matita.interpretations[i].desc = desc; - - var choice = document.createElement("input"); - choice.setAttribute("type","radio"); - choice.setAttribute("name","interpr"); - choice.setAttribute("href",href); - choice.setAttribute("title",title); - if (i == 0) choice.setAttribute("checked",""); - - disambcell.appendChild(choice); - disambcell.appendChild(document.createTextNode(desc)); - disambcell.appendChild(document.createElement("br")); - } + disambcell.appendChild(okbutton); + disambcell.appendChild(cancelbutton); - var okbutton = document.createElement("input"); - okbutton.setAttribute("type","button"); - okbutton.setAttribute("value","OK"); - okbutton.setAttribute("onclick","do_disambiguate()"); - var cancelbutton = document.createElement("input"); - cancelbutton.setAttribute("type","button"); - cancelbutton.setAttribute("value","Cancel"); - cancelbutton.setAttribute("onclick","cancel_disambiguate()"); + disable_toparea(); - disambcell.appendChild(okbutton); - disambcell.appendChild(cancelbutton); + 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); + throw "Stop"; + } + else { + var error = xml.getElementsByTagName("error")[0]; + unlocked.innerHTML = error.childNodes[0].wholeText; + // debug(xml.childNodes[0].nodeValue); + throw "Stop"; + } - disable_toparea(); +} - matita.disambMode = true; - updateSide(); - } - else if (is_defined(disamberr)) { - set_cps(disamberr.childNodes); - matita.unlockedbackup = unlocked.innerHTML.html_to_matita(); - matita.disambMode = true; - disable_toparea(); - next_cp(0); - } - else { - var error = xml.getElementsByTagName("error")[0]; - unlocked.innerHTML = error.childNodes[0].wholeText; - // debug(xml.childNodes[0].nodeValue); - } +function advanceForm1() +{ + processor = function(xml) { + try { + if (is_defined(xml)) { + advOneStep(xml); + populate_goalarray(metasenv); + init_autotraces(); } else { debug("advance failed"); } - resume(); + } catch (e) { + // nothing to do + }; + resume(); }; pause(); callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape()); @@ -984,6 +997,7 @@ function gotoTop() callServer("top",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape()); } + function gotoPos(offset) { if (!is_defined(offset)) { @@ -991,6 +1005,8 @@ function gotoPos(offset) } processor = function(xml) { if (is_defined(xml)) { + try { + /* parsed = xml.getElementsByTagName("parsed")[0]; len = parseInt(parsed.getAttribute("length")); // len0 = unlocked.innerHTML.length; @@ -1008,6 +1024,8 @@ function gotoPos(offset) statements = listcons(len2,statements); unlocked.scrollIntoView(true); // la populate non andrebbe fatta a ogni passo + */ + var len = advOneStep(xml); if (offset <= len) { init_autotraces(); populate_goalarray(metasenv); @@ -1015,6 +1033,11 @@ function gotoPos(offset) } else { gotoPos(offset - len); } + } catch (er) { + init_autotraces(); + populate_goalarray(metasenv); + resume(); + } } else { init_autotraces(); unlocked.scrollIntoView(true);