X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=fb6c0869da5b9c6afac25648187987195215b07c;hb=d8bc6fd4ab18f2995624c75e2889318237e9c17f;hp=a5bf84adcd4610afdd532a35767654ec81434671;hpb=1bc3859b556a1fa1ddfc83f51f93c17eba40eac7;p=helm.git diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index a5bf84adc..fb6c0869d 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -40,12 +40,143 @@ function initialize() // 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 + // but google chrome's innerText is, in a sense, "write only" + // what should we do? logarea.innerText = txt + "\n" + logarea.innerText; } @@ -218,15 +349,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)); } @@ -318,13 +467,15 @@ 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")); + parsed = xml.getElementsByTagName("parsed")[0]; + len = parseInt(parsed.getAttribute("length")); len0 = unlocked.innerHTML.length; - unescaped = unlocked.innerHTML.unescapeHTML(); - parsedtxt = unescaped.substr(0,len); + 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; + locked.innerHTML = locked.innerHTML + parsedtxt; //.matita_to_html(); + unlocked.innerHTML = unparsedtxt.matita_to_html(); len1 = unlocked.innerHTML.length; len2 = len0 - len1; metasenv = xml.getElementsByTagName("meta"); @@ -337,7 +488,7 @@ function advanceForm1() resume(); }; pause(); - callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape()); + callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape()); } @@ -346,13 +497,15 @@ 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")); + parsed = xml.getElementsByTagName("parsed")[0]; + len = parseInt(parsed.getAttribute("length")); len0 = unlocked.innerHTML.length; - unescaped = unlocked.innerHTML.unescapeHTML(); - parsedtxt = unescaped.substr(0,len); + 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; + locked.innerHTML = locked.innerHTML + parsedtxt; //.matita_to_html(); + unlocked.innerHTML = unparsedtxt.matita_to_html(); len1 = unlocked.innerHTML.length; len2 = len0 - len1; metasenv = xml.getElementsByTagName("meta"); @@ -365,7 +518,7 @@ function gotoBottom() resume(); }; pause(); - callServer("bottom",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape()); + callServer("bottom",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape()); } @@ -377,14 +530,15 @@ 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")); + parsed = xml.getElementsByTagName("parsed")[0]; + len = parseInt(parsed.getAttribute("length")); len0 = unlocked.innerHTML.length; - unescaped = unlocked.innerHTML.unescapeHTML(); - parsedtxt = unescaped.substr(0,len); + 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; + locked.innerHTML = locked.innerHTML + parsedtxt; //.matita_to_html(); + unlocked.innerHTML = unparsedtxt.matita_to_html(); len1 = unlocked.innerHTML.length; len2 = len0 - len1; metasenv = xml.getElementsByTagName("meta"); @@ -405,7 +559,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() @@ -447,6 +601,23 @@ function openFile() callServer("open",processor,"file=" + escape(filename.value)); } +function retrieveFile(thefile) +{ + processor = function(xml) + { + if (is_defined(xml)) { + locked.innerHTML = ""; + debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue); + unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue; + + } else { + debug("file open failed"); + } + }; + dialogBox.style.display = "none"; + callServer("open",processor,"file=" + escape(thefile)); +} + function showLibrary() { var req = null; @@ -478,7 +649,7 @@ function showLibrary() if(stat == 200) { debug(req.responseText); - showDialog("Library",req.responseText); + showDialog("

Library

",req.responseText); } } }; @@ -501,7 +672,6 @@ function showSequent() { } function showDialog(title,content) { - dialogTitle.innerHTML = title; dialogContent.innerHTML = content; dialogBox.style.display = "block"; @@ -512,19 +682,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);