X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=f0563928234812f20f980c467fc9b671784a1e6a;hb=0fdf8cd395b21ec003569383aee1449a6fe4b35a;hp=ec19562b248e819a0ab1bb3fb25e35aa59c318d1;hpb=d943958c6e0286068056a74fbb4e98349227420c;p=helm.git diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index ec19562b2..f05639282 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -17,11 +17,28 @@ var dialogContent; var metasenv = ""; var lockedbackup = ""; +function text_of_html(h) +{ + if(document.all) { + return h.innerText; + } else { + return h.textContent; + } +} + +function unescape_html(s) +{ + u = document.getElementById("unescape"); + u.innerHTML = s; + return text_of_html(u) +} + function initialize() { if (readCookie("session") == null) { window.location = "/login.html" } else { + matitaTitle = document.getElementById("matitaTitle"); locked = document.getElementById("locked"); unlocked = document.getElementById("unlocked"); workarea = document.getElementById("workarea"); @@ -38,6 +55,8 @@ function initialize() dialogBox = document.getElementById("dialogBox"); dialogTitle = document.getElementById("dialogTitle"); dialogContent = document.getElementById("dialogContent"); + + changeFile("test.ma"); // hide sequent view at start hideSequent(); @@ -47,6 +66,11 @@ function initialize() } } +function changeFile(name) { + current_fname = name; + matitaTitle.innerHTML = "Matita - cic:/matita/" + name; +} + function init_keyboard(target) { if (target.addEventListener) @@ -109,28 +133,25 @@ function suppressdefault(e,flag) return !flag; } -function restoreSelection(adjust) { +function restoreSelection(r) { unlocked.focus(); - if (savedRange != null) { + if (r != 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); + s.addRange(r); } else if (document.createRange)//non IE and no selection { - window.getSelection().addRange(savedRange); + window.getSelection().addRange(r); } else if (document.selection)//IE { - savedRange.select(); + r.select(); } } } @@ -151,16 +172,24 @@ function keypress(e) 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); + sym = unescape_html(lookup_tex(match)); + if (sym != "undefined") { + if (window.getSelection) { // non IE + savedRange.setStart(savedsc,savedso - (j-i)); + savedRange.deleteContents(); + savedRange.insertNode(document.createTextNode(sym)); + savedsc.parentNode.normalize(); + if (savedRange.collapsed) { // Mozilla + savedRange.setEnd(savedsc,savedRange.endOffset + sym.length); + } + savedRange.collapse(false); + } else { + savedRange.moveStart(i-j); + savedRange.text(sym); + savedRange.collapse(false); + } + restoreSelection(savedRange); + return suppressdefault(e,true); } else { // restoreSelection(0); @@ -173,13 +202,24 @@ function keypress(e) } } +var logtxt = ""; + function debug(txt) { // internet explorer (v.9) doesn't work with innerHTML // 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; + logtxt = logtxt + "\n" + txt; +} + +function showLog() { + logWin = window.open( "", "Matita Log", + "width=600,height=450,status,scrollbars,resizable,screenX=20,screenY=40,left=20,top=40"); + logWin.document.write('Matita Log' + ''); + logWin.document.write(''); + logWin.document.close(); } function listhd(l) @@ -360,12 +400,14 @@ String.prototype.html_to_matita = function() var patt3 = />/gi var patt4 = /</gi; var patt5 = />/gi; + var patt6 = / /gi; var result = this; result = result.replace(patt1,"\n"); result = result.replace(patt2,"\005"); result = result.replace(patt3,"\006"); result = result.replace(patt4,"<"); result = result.replace(patt5,">"); + result = result.replace(patt6," "); return (unescape(result)); } @@ -535,6 +577,35 @@ function gotoBottom() } +function gotoTop() +{ + processor = function(xml) { + if (is_defined(xml)) { + if (xml.childNodes[0].textContent != "ok") { + debug("goto top failed"); + } + else + statements = listnil(); + /* + lockedlen = locked.innerHTML.length - statementlen; + statement = locked.innerHTML.substr(lockedlen, statementlen); + locked.innerHTML = locked.innerHTML.substr(0,lockedlen); + unlocked.innerHTML = statement + unlocked.innerHTML; + */ + unlocked.innerHTML = lockedbackup + unlocked.innerHTML; + lockedbackup = ""; + locked.innerHTML = lockedbackup; + hideSequent(); + unlocked.scrollIntoView(true); + } else { + debug("goto top failed"); + } + resume(); + }; + pause(); + callServer("top",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape()); + +} function gotoPos(offset) { if (!is_defined(offset)) { @@ -627,26 +698,31 @@ function retrieveFile(thefile) processor = function(xml) { if (is_defined(xml)) { + changeFile(thefile); 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; + if (document.all) { // IE + unlocked.innerHTML = xml.childNodes[0].text; + } else { + 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) +function showLibrary(title,callback,reloadDialog) { - var req = null; + var req = null; + dialogBox.reload = reloadDialog; // pause(); if (window.XMLHttpRequest) { @@ -675,7 +751,7 @@ function showLibrary(title,callback) if(stat == 200) { debug(req.responseText); - showDialog("

" + title + "

",req.responseText, callback); + showDialog("

" + title + "

",req.responseText, callback); } } }; @@ -685,10 +761,40 @@ function showLibrary(title,callback) } +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); + showLibrary("Open file", callback, openDialog); } function saveDialog() @@ -700,22 +806,22 @@ function saveDialog() (unlocked.innerHTML.html_to_matita()).sescape(), false,saveDialog); }; - showLibrary("Save file as", callback); + showLibrary("Save file as", callback, saveDialog); } function newDialog() { callback = function (fname) { dialogBox.style.display = "none"; - saveFile(fname,"","",false,newDialog); - retrieveFile(fname); + saveFile(fname,"","",false,newDialog,true); }; - showLibrary("Create new file", callback); + showLibrary("Create new file", callback, newDialog); } -function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog) +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(); @@ -727,13 +833,14 @@ function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog) 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); + saveFile(fname,lockedtxt,unlockedtxt,true,reloadDialog,reloadFile); } else { reloadDialog(); } } else { - current_fname = fname; + changeFile(fname); debug("file saved!"); + if (reloadFile) { retrieveFile(fname); } } } else { debug("save file failed"); @@ -750,13 +857,37 @@ function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog) else { debug("no file selected"); } } +function createDir() { + abortDialog(); + dirname = prompt("New directory name:\ncic:/matita/","newdir"); + if (dirname != null) { + processor = function(xml) { + if (is_defined(xml)) { + if (xml.childNodes[0].textContent != "ok") { + alert("An error occurred :-("); + } + } else { + alert("An error occurred :-("); + } + dialogBox.reload(); + }; + pause(); + callServer("save",processor,"file=" + escape(dirname) + + "&locked=&unlocked=&force=false&dir=true"); + } else { + dialogBox.reload(); + } +} + function commitAll() { processor = function(xml) { if (is_defined(xml)) { - debug("commit succeeded(?)"); + debug(xml.getElementsByTagName("details")[0].textContent); + alert("Commit executed: see details in the log.\n\n" + + "NOTICE: this message does NOT imply (yet) that the commit was successful."); } else { - debug("commit failed!"); + alert("Commit failed!"); } resume(); }; @@ -764,23 +895,51 @@ function commitAll() callServer("commit",processor); } +function updateAll() +{ + processor = function(xml) { + if (is_defined(xml)) { + alert("Update executed.\n\n" + + "Details:\n" + + xml.getElementsByTagName("details")[0].textContent); + } else { + alert("Update failed!"); + } + resume(); + }; + pause(); + callServer("update",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.style.display = "block"; dialogBox.callback = callback; + dialogBox.style.display = "block"; +} + +function abortDialog() { + dialogBox.style.display = "none"; +} + +function abortUpload() { + uploadBox.style.display = "none"; } function removeElement(id) {