X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=3b37fc76b0abf1537fc06203b5bda68274163b4a;hb=54f0752c831479f87d61afcdfdafd2a35edb4053;hp=d9bd38aa80e94dac072b197f10cb86b1d0555032;hpb=93ad0bc98a502397b5ba0334c0f7088da045fa2d;p=helm.git diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index d9bd38aa8..3b37fc76b 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -17,6 +17,22 @@ 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) { @@ -109,28 +125,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 +164,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 +194,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('