X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=837c687cb9385dc22af1948d924a041deb6b997e;hb=9dac2c325dca1b5b92d6ba11dadf470538bae28e;hp=423eda674bbd1ed06c54d379dd65e56b5fb78f24;hpb=2ab54291cd9038c81b82ddb29936e966c66a480c;p=helm.git diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index 423eda674..837c687cb 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -11,7 +11,11 @@ var advanceButton; var retractButton; var cursorButton; var bottomButton; +var dialogBox; +var dialogTitle; +var dialogContent; var metasenv = ""; +var lockedbackup = ""; function initialize() { @@ -31,16 +35,151 @@ function initialize() retractButton = document.getElementById("retract"); cursorButton = document.getElementById("cursor"); bottomButton = document.getElementById("bottom"); + dialogBox = document.getElementById("dialogBox"); + dialogTitle = document.getElementById("dialogTitle"); + dialogContent = document.getElementById("dialogContent"); // hide sequent view at start hideSequent(); + + // initialize keyboard events in the unlocked script + init_keyboard(unlocked); } } +function init_keyboard(target) +{ + if (target.addEventListener) + { +// target.addEventListener("keydown",keydown,false); + target.addEventListener("keypress",keypress,false); +// target.addEventListener("keyup",keyup,false); +// target.addEventListener("textInput",textinput,false); + } + else if (target.attachEvent) + { +// target.attachEvent("onkeydown", keydown); + target.attachEvent("onkeypress", keypress); +// target.attachEvent("onkeyup", keyup); +// target.attachEvent("ontextInput", textinput); + } + else + { +// target.onkeydown= keydown; + target.onkeypress= keypress; +// target.onkeyup= keyup; +// target.ontextinput= textinput; // probably doesn't work + } + +} + +function keyval(n) +{ + if (n == null) return 'undefined'; + var s= '' + n; + if (n >= 32 && n < 127) s+= ' (' + String.fromCharCode(n) + ')'; + while (s.length < 9) s+= ' '; + return s; +} + +function string_of_key(n) +{ + if (n == null) return 'undefined'; + return String.fromCharCode(n); +} + +function pressmesg(w,e) +{ + debug(w + ' keyCode=' + keyval(e.keyCode) + + ' which=' + keyval(e.which) + + ' charCode=' + keyval(e.charCode) + + '\n shiftKey='+e.shiftKey + + ' ctrlKey='+e.ctrlKey + + ' altKey='+e.altKey + + ' metaKey='+e.metaKey); +} + +function suppressdefault(e,flag) +{ + if (flag) + { + if (e.preventDefault) e.preventDefault(); + if (e.stopPropagation) e.stopPropagation(); + } + return !flag; +} + +function restoreSelection(adjust) { + unlocked.focus(); + if (savedRange != null) { + if (window.getSelection)//non IE and there is already a selection + { + var s = window.getSelection(); + if (s.rangeCount > 0) + s.removeAllRanges(); + range = document.createRange(); + range.setStart(savedsc,savedso + adjust); + range.collapse(true); + s.addRange(range); + } + else + if (document.createRange)//non IE and no selection + { + window.getSelection().addRange(savedRange); + } + else + if (document.selection)//IE + { + savedRange.select(); + } + } +} + +function lookup_tex(texmacro) +{ + texmacro = texmacro.substring(1); + return unescape(macro2utf8[texmacro]); +} + +function keypress(e) +{ + if (!e) e= event; + pressmesg('keypress',e); + var s = string_of_key(e.charCode); + if (s == " ") { + j = getCursorPos(); + i = unlocked.innerHTML.lastIndexOf('\\',j); + if (i >= 0) { + match = unlocked.innerHTML.substring(i,j); + pre = unlocked.innerHTML.substring(0,i); + post = unlocked.innerHTML.substring(j); + + sym = lookup_tex(match); + if (typeof sym != "undefined") { + len1 = unlocked.innerText.length; + unlocked.innerHTML = pre + sym + post; + len2 = unlocked.innerText.length; + restoreSelection(len2 - len1); + return suppressdefault(e,true); + } + else { + // restoreSelection(0); + return suppressdefault(e,false); + } + } + else return suppressdefault(e,false); + } else { + return suppressdefault(e,false); + } +} + function debug(txt) { // internet explorer (v.9) doesn't work with innerHTML - logarea.innerText = txt + "\n" + logarea.innerText; + // but google chrome's innerText is, in a sense, "write only" + // what should we do? + // logarea.innerText = txt + "\n" + logarea.innerText; + logarea.innerHTML = txt; // + "\n" + logarea.innerText; } function listhd(l) @@ -199,6 +338,8 @@ function switch_goal(meta) } } +// the following is used to avoid escaping unicode, which results in +// the server being unable to unescape the string String.prototype.sescape = function() { var patt1 = /%/gi; var patt2 = /=/gi; @@ -212,15 +353,33 @@ String.prototype.sescape = function() { return (result); } -String.prototype.unescapeHTML = function() +String.prototype.html_to_matita = function() { var patt1 = //gi; - var patt2 = /</gi; - var patt3 = />/gi; + var patt2 = //gi + var patt4 = /</gi; + var patt5 = />/gi; var result = this; result = result.replace(patt1,"\n"); - result = result.replace(patt2,"<"); - result = result.replace(patt3,">"); + result = result.replace(patt2,"\005"); + result = result.replace(patt3,"\006"); + result = result.replace(patt4,"<"); + result = result.replace(patt5,">"); + return (unescape(result)); +} + +String.prototype.matita_to_html = function() +{ + var patt1 = //gi + var patt3 = /\005/gi; + var patt4 = /\006/gi; + var result = this; + result = result.replace(patt1,"<"); + result = result.replace(patt2,">"); + result = result.replace(patt3,"<"); + result = result.replace(patt4,">"); return (unescape(result)); } @@ -312,15 +471,19 @@ function advanceForm1() processor = function(xml) { if (is_defined(xml)) { // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND"); - len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length")); - len0 = unlocked.innerHTML.length; - unescaped = unlocked.innerHTML.unescapeHTML(); - parsedtxt = unescaped.substr(0,len); + parsed = xml.getElementsByTagName("parsed")[0]; + len = parseInt(parsed.getAttribute("length")); + // len0 = unlocked.innerHTML.length; + unescaped = unlocked.innerHTML.html_to_matita(); + parsedtxt = parsed.childNodes[0].nodeValue; + //parsedtxt = unescaped.substr(0,len); unparsedtxt = unescaped.substr(len); - locked.innerHTML = locked.innerHTML + parsedtxt; - unlocked.innerHTML = unparsedtxt; - len1 = unlocked.innerHTML.length; - len2 = len0 - len1; + 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"); populate_goalarray(metasenv); statements = listcons(len2,statements); @@ -331,7 +494,7 @@ function advanceForm1() resume(); }; pause(); - callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape()); + callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape()); } @@ -340,26 +503,34 @@ function gotoBottom() processor = function(xml) { if (is_defined(xml)) { // debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND"); - len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length")); - len0 = unlocked.innerHTML.length; - unescaped = unlocked.innerHTML.unescapeHTML(); - parsedtxt = unescaped.substr(0,len); - unparsedtxt = unescaped.substr(len); - locked.innerHTML = locked.innerHTML + parsedtxt; - unlocked.innerHTML = unparsedtxt; - len1 = unlocked.innerHTML.length; - len2 = len0 - len1; - metasenv = xml.getElementsByTagName("meta"); - populate_goalarray(metasenv); - statements = listcons(len2,statements); - unlocked.scrollIntoView(true); + parsed = xml.getElementsByTagName("parsed")[0]; + len = parseInt(parsed.getAttribute("length")); + if (len > 0) { + // len0 = unlocked.innerHTML.length; + unescaped = unlocked.innerHTML.html_to_matita(); + // not working in mozilla + // parsedtxt = parsed.childNodes[0].nodeValue; + parsedtxt = parsed.childNodes[0].wholeText; + //parsedtxt = unescaped.substr(0,len); + unparsedtxt = unescaped.substr(len); + lockedbackup += parsedtxt; + locked.innerHTML = lockedbackup; //.matita_to_html(); + unlocked.innerHTML = unparsedtxt.matita_to_html(); + // len1 = unlocked.innerHTML.length; + len2 = parsedtxt.length; + metasenv = xml.getElementsByTagName("meta"); + populate_goalarray(metasenv); + if (len2 > 0) + statements = listcons(len2,statements); + unlocked.scrollIntoView(true); + } } else { debug("goto bottom failed"); } resume(); }; pause(); - callServer("bottom",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape()); + callServer("bottom",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape()); } @@ -371,16 +542,18 @@ function gotoPos(offset) } processor = function(xml) { if (is_defined(xml)) { - // debug("goto pos: received response\nBEGIN\n" + req.responseText + "\nEND"); - len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length")); - len0 = unlocked.innerHTML.length; - unescaped = unlocked.innerHTML.unescapeHTML(); - parsedtxt = unescaped.substr(0,len); + parsed = xml.getElementsByTagName("parsed")[0]; + len = parseInt(parsed.getAttribute("length")); + // len0 = unlocked.innerHTML.length; + unescaped = unlocked.innerHTML.html_to_matita(); + parsedtxt = parsed.childNodes[0].nodeValue; + //parsedtxt = unescaped.substr(0,len); unparsedtxt = unescaped.substr(len); - locked.innerHTML = locked.innerHTML + parsedtxt; - unlocked.innerHTML = unparsedtxt; - len1 = unlocked.innerHTML.length; - len2 = len0 - len1; + lockedbackup += parsedtxt; + locked.innerHTML = lockedbackup; //.matita_to_html(); + unlocked.innerHTML = unparsedtxt.matita_to_html(); + // len1 = unlocked.innerHTML.length; + len2 = parsedtxt.length; metasenv = xml.getElementsByTagName("meta"); // populate_goalarray(metasenv); statements = listcons(len2,statements); @@ -399,7 +572,7 @@ function gotoPos(offset) } } pause(); - callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape()); + callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape()); } function retract() @@ -409,10 +582,17 @@ function retract() // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND"); statementlen = parseInt(listhd(statements)); statements = listtl(statements); + /* lockedlen = locked.innerHTML.length - statementlen; statement = locked.innerHTML.substr(lockedlen, statementlen); locked.innerHTML = locked.innerHTML.substr(0,lockedlen); unlocked.innerHTML = statement + unlocked.innerHTML; + */ + lockedlen = lockedbackup.length - statementlen; + statement = lockedbackup.substr(lockedlen, statementlen); + lockedbackup = lockedbackup.substr(0,lockedlen); + locked.innerHTML = lockedbackup; + unlocked.innerHTML = statement + unlocked.innerHTML; metasenv = xml.getElementsByTagName("meta"); populate_goalarray(metasenv); unlocked.scrollIntoView(true); @@ -432,8 +612,9 @@ function openFile() processor = function(xml) { if (is_defined(xml)) { - locked.innerHTML = ""; - unlocked.innerHTML = xml.documentElement.textContent; + lockedbackup = ""; + locked.innerHTML = lockedbackup; + unlocked.innerHTML = xml.documentElement.wholeText; } else { debug("file open failed"); } @@ -441,16 +622,208 @@ function openFile() callServer("open",processor,"file=" + escape(filename.value)); } +function retrieveFile(thefile) +{ + processor = function(xml) + { + if (is_defined(xml)) { + lockedbackup = "" + locked.innerHTML = lockedbackup; + // code originally used in google chrome (problems with mozilla) + // debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue); + // unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue; + debug(xml.childNodes[0].textContent); + unlocked.innerHTML = xml.childNodes[0].textContent; + + } else { + debug("file open failed"); + } + }; + dialogBox.style.display = "none"; + current_fname = thefile; + callServer("open",processor,"file=" + escape(thefile)); +} + +function showLibrary(title,callback) +{ + var req = null; + // pause(); + if (window.XMLHttpRequest) + { + req = new XMLHttpRequest(); + } + else if (window.ActiveXObject) + { + try { + req = new ActiveXObject("Msxml2.XMLHTTP"); + } catch (e) + { + try { + req = new ActiveXObject("Microsoft.XMLHTTP"); + } catch (e) {} + } + } + req.onreadystatechange = function() + { + + rs = req.readyState; + + if(rs == 4) + { + stat = req.status; + stxt = req.statusText; + if(stat == 200) + { + debug(req.responseText); + showDialog("

" + title + "

",req.responseText, callback); + } + } + }; + req.open("POST", "viewlib"); // + escape(unlocked.innerHTML), true); + req.setRequestHeader("Content-type","application/x-www-form-urlencoded"); + req.send(); + +} + +function uploadDialog() +{ + uploadBox.style.display = "block"; +} + +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"; +// } +// } +} + +function openDialog() +{ + callback = function (fname) { retrieveFile(fname); }; + showLibrary("Open file", callback); +} + +function saveDialog() +{ + callback = function (fname) { + dialogBox.style.display = "none"; + saveFile(fname, + (locked.innerHTML.html_to_matita()).sescape(), + (unlocked.innerHTML.html_to_matita()).sescape(), + false,saveDialog); + }; + showLibrary("Save file as", callback); +} + +function newDialog() +{ + callback = function (fname) { + dialogBox.style.display = "none"; + saveFile(fname,"","",false,newDialog,true); + }; + showLibrary("Create new file", callback); +} + + +function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog,reloadFile) +{ + if (!is_defined(reloadFile)) { reloadFile = true }; + if (!is_defined(fname)) { + fname = current_fname; + lockedtxt = (locked.innerHTML.html_to_matita()).sescape(); + unlockedtxt = (unlocked.innerHTML.html_to_matita()).sescape(); + force = true; + // when force is true, reloadDialog is not needed + } + processor = function(xml) { + if (is_defined(xml)) { + if (xml.childNodes[0].textContent != "ok") { + if (confirm("File already exists. All existing data will be lost.\nDo you want to proceed anyway?")) { + saveFile(fname,lockedtxt,unlockedtxt,true,reloadDialog,reloadFile); + } else { + reloadDialog(); + } + } else { + current_fname = fname; + debug("file saved!"); + if (reloadFile) { retrieveFile(fname); } + } + } else { + debug("save file failed"); + } + resume(); + }; + if (is_defined(fname)) { + pause(); + callServer("save",processor,"file=" + escape(fname) + + "&locked=" + lockedtxt + + "&unlocked=" + unlockedtxt + + "&force=" + force); + } + else { debug("no file selected"); } +} + +function commitAll() +{ + processor = function(xml) { + if (is_defined(xml)) { + debug("commit succeeded(?)"); + } else { + debug("commit failed!"); + } + resume(); + }; + pause(); + callServer("commit",processor); +} + var goalcell; function hideSequent() { - goalcell.parentNode.removeChild(goalcell); - scriptcell.setAttribute("colspan","2"); + goalcell.style.display = "none"; + scriptcell.style.width = "100%"; + scriptcell.style.minWidth = "100%"; + scriptcell.style.maxWidth = "100%"; } function showSequent() { - scriptcell.setAttribute("colspan","1"); - workarea.appendChild(goalcell); + scriptcell.style.width = "67%"; + scriptcell.style.minWidth = "67%"; + scriptcell.style.maxWidth = "67%"; + goalcell.style.display = "inline-block"; +} + +function showDialog(title,content,callback) { + dialogTitle.innerHTML = title; + dialogContent.innerHTML = content; + dialogBox.callback = callback; + dialogBox.style.display = "block"; +} + +function abortDialog() { + dialogBox.style.display = "none"; +} + +function abortUpload() { + uploadBox.style.display = "none"; } function removeElement(id) { @@ -458,19 +831,24 @@ function removeElement(id) { element.parentNode.removeChild(element); } +var savedsc; +var savedso; + function getCursorPos() { var cursorPos; if (window.getSelection) { var selObj = window.getSelection(); - var selRange = selObj.getRangeAt(0); + savedRange = selObj.getRangeAt(0); + savedsc = savedRange.startContainer; + savedso = savedRange.startOffset; //cursorPos = findNode(selObj.anchorNode.parentNode.childNodes, selObj.anchorNode) + selObj.anchorOffset; cursorPos = findNode(unlocked.childNodes, selObj.anchorNode,0) + selObj.anchorOffset; /* FIXME the following works wrong in Opera when the document is longer than 32767 chars */ return(cursorPos); } else if (document.selection) { - var range = document.selection.createRange(); - var bookmark = range.getBookmark(); + savedRange = document.selection.createRange(); + var bookmark = savedRange.getBookmark(); /* FIXME the following works wrong when the document is longer than 65535 chars */ cursorPos = bookmark.charCodeAt(2) - 11; /* Undocumented function [3] */ return(cursorPos);