X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=890b34ec0b8cef0982f5b703e35ce8470130b30d;hb=0e3d8e00433a9a4dd72310c1e889814848a96c10;hp=ccb2f37445fabf8e38332df2fc714e9d5fffbf6e;hpb=988cf01c5bd740d6e75767327f201a3c43d635ed;p=helm.git diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index ccb2f3744..890b34ec0 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -16,6 +16,7 @@ var dialogTitle; var dialogContent; var metasenv = ""; var lockedbackup = ""; +var matita; function text_of_html(h) { @@ -48,11 +49,17 @@ function initialize() if (readCookie("session") == null) { window.location = "/login.html" } else { + body = document.body; + titlebar = document.getElementById("titlebar"); matitaTitle = document.getElementById("matitaTitle"); + apparea = document.getElementById("matitaapparea"); locked = document.getElementById("locked"); unlocked = document.getElementById("unlocked"); + toparea = document.getElementById("toparea"); workarea = document.getElementById("workarea"); scriptcell = document.getElementById("scriptcell"); + sidearea = document.getElementById("sidearea"); + disambcell = document.getElementById("disambcell"); goalcell = document.getElementById("goalcell"); goals = document.getElementById("goals"); goalview = document.getElementById("goalview"); @@ -63,13 +70,18 @@ function initialize() cursorButton = document.getElementById("cursor"); bottomButton = document.getElementById("bottom"); dialogBox = document.getElementById("dialogBox"); + uploadBox = document.getElementById("uploadBox"); dialogTitle = document.getElementById("dialogTitle"); dialogContent = document.getElementById("dialogContent"); - changeFile("test.ma"); - + matita = new Object(); + matita.disambMode = matita.proofMode = false; + // hide sequent view at start - hideSequent(); + initializeLayout(); + updateSide(); + + changeFile("test.ma"); // initialize keyboard events in the unlocked script init_keyboard(unlocked); @@ -535,28 +547,87 @@ function advanceForm1() { processor = function(xml) { if (is_defined(xml)) { - parsed = xml.getElementsByTagName("parsed")[0]; + var parsed = xml.getElementsByTagName("parsed")[0]; + var ambiguity = xml.getElementsByTagName("ambiguity")[0]; if (is_defined(parsed)) { // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND"); - len = parseInt(parsed.getAttribute("length")); + var len = parseInt(parsed.getAttribute("length")); // len0 = unlocked.innerHTML.length; - unescaped = unlocked.innerHTML.html_to_matita(); - parsedtxt = parsed.childNodes[0].nodeValue; + var unescaped = unlocked.innerHTML.html_to_matita(); + var parsedtxt = parsed.childNodes[0].nodeValue; //parsedtxt = unescaped.substr(0,len); - unparsedtxt = unescaped.substr(len); + var unparsedtxt = unescaped.substr(len); lockedbackup += parsedtxt; locked.innerHTML = lockedbackup; unlocked.innerHTML = unparsedtxt.matita_to_html(); // len1 = unlocked.innerHTML.length; // len2 = len0 - len1; - len2 = parsedtxt.length; - metasenv = xml.getElementsByTagName("meta"); + var len2 = parsedtxt.length; + var metasenv = xml.getElementsByTagName("meta"); populate_goalarray(metasenv); 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; + matita.interpretations = []; + + var unlockedtxt = unlocked.innerHTML; + var pre = unlockedtxt.substring(0,start); + var mid = unlockedtxt.substring(start,stop); + var post = unlockedtxt.substring(stop); + 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 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","void(0)"); + + disambcell.appendChild(okbutton); + disambcell.appendChild(cancelbutton); + + matita.disambMode = true; + updateSide(); + } else { - error = xml.getElementsByTagName("error")[0]; + var error = xml.getElementsByTagName("error")[0]; unlocked.innerHTML = error.childNodes[0].nodeValue; // debug(xml.childNodes[0].nodeValue); } @@ -944,17 +1015,13 @@ function updateAll() var goalcell; function hideSequent() { - goalcell.style.display = "none"; - scriptcell.style.width = "100%"; - scriptcell.style.minWidth = "100%"; - scriptcell.style.maxWidth = "100%"; + matita.proofMode = false; + updateSide(); } function showSequent() { - scriptcell.style.width = "67%"; - scriptcell.style.minWidth = "67%"; - scriptcell.style.maxWidth = "67%"; - goalcell.style.display = "inline-block"; + matita.proofMode = true; + updateSide(); } function showDialog(title,content,callback) { @@ -964,12 +1031,13 @@ function showDialog(title,content,callback) { dialogBox.style.display = "block"; } -function abortDialog() { - dialogBox.style.display = "none"; +function showDisamb(content) { + disambContent.innerHTML = content; + disambBox.style.display = "block"; } -function abortUpload() { - uploadBox.style.display = "none"; +function abortDialog(dialog) { + dialogBox.style.display = "none"; } function removeElement(id) { @@ -1028,6 +1096,39 @@ function test () { debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos())); } +function get_checked_index(name) { + var radios = document.getElementsByName(name); + for (i = 0; i < radios.length; i++) { + if (radios[i].checked) { + return i; + } + } + return null; +} + +function do_disambiguate() { + var i = get_checked_index("interpr"); + if (i != null) { + var pre = matita.unlockedbackup.substring(0,matita.ambiguityStart); + var mid = matita.unlockedbackup.substring(matita.ambiguityStart,matita.ambiguityStop); + var post = matita.unlockedbackup.substring(matita.ambiguityStop); + + var href = matita.interpretations[i].href; + var title = matita.interpretations[i].title; + + if (is_defined(title)) { + mid = "" + mid + ""; + } else { + mid = "" + mid + ""; + } + + unlocked.innerHTML = pre + mid + post; + + matita.disambMode = false; + updateSide(); + } +} + function readCookie(name) { var nameEQ = name + "="; var ca = document.cookie.split(';');