X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=fb6c0869da5b9c6afac25648187987195215b07c;hb=d8bc6fd4ab18f2995624c75e2889318237e9c17f;hp=d0b5ce21768f22ae8ffaf6671f68fc2e8779a10d;hpb=3de3e8330cc51cb62adba7c6d806ef2711b5933a;p=helm.git diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index d0b5ce217..fb6c0869d 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -81,12 +81,18 @@ function keyval(n) 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)); - debug(' shiftKey='+e.shiftKey + ' charCode=' + keyval(e.charCode) + + '\n shiftKey='+e.shiftKey + ' ctrlKey='+e.ctrlKey + ' altKey='+e.altKey + ' metaKey='+e.metaKey); @@ -101,17 +107,76 @@ function suppressdefault(e,flag) } 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); - return suppressdefault(e,/*document.testform.keypress.checked*/ false); + 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; } @@ -284,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)); } @@ -384,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"); @@ -403,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()); } @@ -412,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"); @@ -431,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()); } @@ -443,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"); @@ -471,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() @@ -519,7 +607,9 @@ function retrieveFile(thefile) { if (is_defined(xml)) { locked.innerHTML = ""; - unlocked.innerHTML = xml.documentElement.textContent; + debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue); + unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue; + } else { debug("file open failed"); } @@ -592,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);