18 var lockedbackup = "";
21 function text_of_html(h)
30 function unescape_html(s)
32 u = document.getElementById("unescape");
34 return text_of_html(u)
37 function filterByClass (elements,class){
38 var itemsfound = new Array;
39 for(var i=0;i<elements.length;i++){
40 if(elements[i].className == class){
41 itemsfound.push(elements[i]);
49 if (readCookie("session") == null) {
50 window.location = "/login.html"
53 titlebar = document.getElementById("titlebar");
54 matitaTitle = document.getElementById("matitaTitle");
55 apparea = document.getElementById("matitaapparea");
56 locked = document.getElementById("locked");
57 unlocked = document.getElementById("unlocked");
58 toparea = document.getElementById("toparea");
59 workarea = document.getElementById("workarea");
60 scriptcell = document.getElementById("scriptcell");
61 sidearea = document.getElementById("sidearea");
62 disambcell = document.getElementById("disambcell");
63 goalcell = document.getElementById("goalcell");
64 goals = document.getElementById("goals");
65 goalview = document.getElementById("goalview");
66 filename = document.getElementById("filename");
67 logarea = document.getElementById("logarea");
68 advanceButton = document.getElementById("advance");
69 retractButton = document.getElementById("retract");
70 cursorButton = document.getElementById("cursor");
71 bottomButton = document.getElementById("bottom");
72 dialogBox = document.getElementById("dialogBox");
73 uploadBox = document.getElementById("uploadBox");
74 dialogTitle = document.getElementById("dialogTitle");
75 dialogContent = document.getElementById("dialogContent");
77 matita = new Object();
78 matita.disambMode = matita.proofMode = false;
80 // hide sequent view at start
84 changeFile("test.ma");
86 // initialize keyboard events in the unlocked script
87 init_keyboard(unlocked);
91 function changeFile(name) {
93 matitaTitle.innerHTML = "Matita - cic:/matita/" + name;
96 function init_keyboard(target)
98 if (target.addEventListener)
100 // target.addEventListener("keydown",keydown,false);
101 target.addEventListener("keypress",keypress,false);
102 // target.addEventListener("keyup",keyup,false);
103 // target.addEventListener("textInput",textinput,false);
105 else if (target.attachEvent)
107 // target.attachEvent("onkeydown", keydown);
108 target.attachEvent("onkeypress", keypress);
109 // target.attachEvent("onkeyup", keyup);
110 // target.attachEvent("ontextInput", textinput);
114 // target.onkeydown= keydown;
115 target.onkeypress= keypress;
116 // target.onkeyup= keyup;
117 // target.ontextinput= textinput; // probably doesn't work
124 if (n == null) return 'undefined';
126 if (n >= 32 && n < 127) s+= ' (' + String.fromCharCode(n) + ')';
127 while (s.length < 9) s+= ' ';
131 function string_of_key(n)
133 if (n == null) return 'undefined';
134 return String.fromCharCode(n);
137 function pressmesg(w,e)
139 debug(w + ' keyCode=' + keyval(e.keyCode) +
140 ' which=' + keyval(e.which) +
141 ' charCode=' + keyval(e.charCode) +
142 '\n shiftKey='+e.shiftKey
143 + ' ctrlKey='+e.ctrlKey
144 + ' altKey='+e.altKey
145 + ' metaKey='+e.metaKey);
148 function suppressdefault(e,flag)
152 if (e.preventDefault) e.preventDefault();
153 if (e.stopPropagation) e.stopPropagation();
158 function restoreSelection(r) {
161 if (window.getSelection)//non IE and there is already a selection
163 var s = window.getSelection();
164 if (s.rangeCount > 0)
169 if (document.createRange)//non IE and no selection
171 window.getSelection().addRange(r);
174 if (document.selection)//IE
181 function lookup_tex(texmacro)
183 texmacro = texmacro.substring(1);
184 return unescape(macro2utf8[texmacro]);
187 function strip_errors()
189 errors = filterByClass(unlocked.getElementsByTagName("span"),"error");
190 for (i = 0; i < errors.length; i++) {
191 children = errors[i].childNodes;
192 for (j = 0; j < children.length; j++) {
193 unlocked.insertBefore(children[j],errors[i]);
195 unlocked.removeChild(errors[i]);
202 pressmesg('keypress',e);
203 var s = string_of_key(e.charCode);
207 i = unlocked.innerHTML.lastIndexOf('\\',j);
209 match = unlocked.innerHTML.substring(i,j);
210 sym = unescape_html(lookup_tex(match));
211 if (sym != "undefined") {
212 if (window.getSelection) { // non IE
213 savedRange.setStart(savedsc,savedso - (j-i));
214 savedRange.deleteContents();
215 savedRange.insertNode(document.createTextNode(sym));
216 savedsc.parentNode.normalize();
217 if (savedRange.collapsed) { // Mozilla
218 savedRange.setEnd(savedsc,savedRange.endOffset + sym.length);
220 savedRange.collapse(false);
222 savedRange.moveStart(i-j);
223 savedRange.text(sym);
224 savedRange.collapse(false);
226 restoreSelection(savedRange);
227 return suppressdefault(e,true);
230 // restoreSelection(0);
231 return suppressdefault(e,false);
234 else return suppressdefault(e,false);
236 return suppressdefault(e,false);
244 // internet explorer (v.9) doesn't work with innerHTML
245 // but google chrome's innerText is, in a sense, "write only"
246 // what should we do?
247 // logarea.innerText = txt + "\n" + logarea.innerText;
248 logtxt = /* logtxt + "\n" +*/ txt;
252 logWin = window.open( "", "Matita Log",
253 "width=600,height=450,status,scrollbars,resizable,screenX=20,screenY=40,left=20,top=40");
254 logWin.document.write('<html><head><title>Matita Log' + '</title></head>');
255 logWin.document.write('<body><textarea style="width:100%;height:100%;">' +
256 logtxt + '</textarea></body></html>');
257 logWin.document.close();
263 debug("hd of '" + l + "' = '" + ar[0] + "'");
271 debug("tl of '" + l + "' = '" + tl + "'");
275 function listcons(x,l)
277 debug("cons '" + x + "' on '" + l + "'");
278 return (x + "#" + l);
291 function fold_left (f,acc,l)
294 { debug("'" + l + "' is fold end");
297 { debug("'" + l + "' is fold cons");
298 return(fold_left (f,f(acc,(listhd(l))),listtl(l))); }
301 function listiter (f,l)
304 { debug("'" + l + "' is nil");
309 debug("'" + l + "' is not nil");
311 listiter(f,listtl(l));
315 function listmap (f,l)
317 debug("listmap on " + l);
319 { debug("returning listnil");
323 { debug("cons f(hd) map(f,tl)");
324 return(f(listhd(l)) + "#" + listmap(f,listtl(l)));
328 var statements = listnil();
331 var metalist = listnil();
333 function pairmap (f,p)
335 debug("pairmap of '" + p + "'");
337 return (f(ar[0],ar[1]));
340 function tripletmap (f,p)
342 debug("tripletmap of '" + p + "'");
344 return (f(ar[0],ar[1],ar[2]));
350 return (pairmap (function (a,b) { return (a); }, p));
356 return (tripletmap (function (a,b,c) { return (a); }, p));
362 return (tripletmap (function (a,b,c) { return (b); }, p));
368 return (tripletmap (function (a,b,c) { return (c); }, p));
371 function populate_goalarray(menv)
373 debug("metasenv.length = " + menv.length);
374 if (menv.length == 0) {
380 goalarray = new Array();
381 metalist = listnil();
382 var tmp_goallist = "";
383 for (i = 0; i < menv.length; i++) {
384 metano = menv[i].getAttribute("number");
385 metaname = menv[i].childNodes[0].childNodes[0].data;
386 goal = menv[i].childNodes[1].childNodes[0].data;
387 debug ("found meta n. " + metano);
388 debug ("found goal\nBEGIN" + goal + "\nEND");
389 goalarray[metano] = goal;
390 tmp_goallist = " <A href=\"javascript:switch_goal(" + metano + ")\">" + metaname + "</A>" + tmp_goallist;
391 metalist = listcons(metano,metalist);
392 debug ("goalarray[\"" + metano + "\"] = " + goalarray[metano]);
394 goals.innerHTML = tmp_goallist;
395 debug("new metalist is '" + metalist + "'");
396 if (is_nil(metalist)) {
400 switch_goal(listhd(metalist));
405 function switch_goal(meta)
407 if (typeof meta == "undefined") {
408 goalview.innerHTML = "";
411 debug("switch_goal " + meta + "\n" + goalarray[meta]);
412 goalview.innerHTML = "<B>Goal ?" + meta + ":</B>\n\n" + goalarray[meta];
416 // the following is used to avoid escaping unicode, which results in
417 // the server being unable to unescape the string
418 String.prototype.sescape = function() {
424 result = result.replace(patt1,"%25");
425 result = result.replace(patt2,"%3D");
426 result = result.replace(patt3,"%26");
427 result = result.replace(patt4,"%2B");
431 String.prototype.html_to_matita = function()
433 var patt1 = /<br(\/|)>/gi;
436 var patt4 = /</gi;
437 var patt5 = />/gi;
438 var patt6 = / /gi;
440 result = result.replace(patt1,"\n");
441 result = result.replace(patt2,"\005");
442 result = result.replace(patt3,"\006");
443 result = result.replace(patt4,"<");
444 result = result.replace(patt5,">");
445 result = result.replace(patt6," ");
446 return (unescape(result));
449 String.prototype.matita_to_html = function()
453 var patt3 = /\005/gi;
454 var patt4 = /\006/gi;
456 result = result.replace(patt1,"<");
457 result = result.replace(patt2,">");
458 result = result.replace(patt3,"<");
459 result = result.replace(patt4,">");
460 return (unescape(result));
465 advanceButton.disabled = true;
466 retractButton.disabled = true;
467 cursorButton.disabled = true;
468 bottomButton.disabled = true;
473 advanceButton.disabled = false;
474 retractButton.disabled = false;
475 cursorButton.disabled = false;
476 bottomButton.disabled = false;
479 function is_defined(x)
481 return (typeof x != "undefined");
484 /* servicename: name of the service being called
485 * reqbody: text of the request
486 * processResponse: processes the server response
487 * (takes the response text in input, undefined in case of error)
489 function callServer(servicename,processResponse,reqbody)
493 if (window.XMLHttpRequest)
495 req = new XMLHttpRequest();
497 else if (window.ActiveXObject)
500 req = new ActiveXObject("Msxml2.XMLHTTP");
504 req = new ActiveXObject("Microsoft.XMLHTTP");
508 req.onreadystatechange = function()
516 stxt = req.statusText;
519 debug(req.responseText);
520 if (window.DOMParser) {
521 parser=new DOMParser();
522 xmlDoc=parser.parseFromString(req.responseText,"text/xml");
524 else // Internet Explorer
526 xmlDoc=new ActiveXObject("Microsoft.XMLDOM");
527 xmlDoc.async="false";
528 xmlDoc.loadXML(req.responseText);
530 processResponse(xmlDoc);
536 req.open("POST", servicename); // + escape(unlocked.innerHTML), true);
537 req.setRequestHeader("Content-type","application/x-www-form-urlencoded");
546 function advanceForm1()
548 processor = function(xml) {
549 if (is_defined(xml)) {
550 var parsed = xml.getElementsByTagName("parsed")[0];
551 var ambiguity = xml.getElementsByTagName("ambiguity")[0];
552 if (is_defined(parsed)) {
553 // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
554 var len = parseInt(parsed.getAttribute("length"));
555 // len0 = unlocked.innerHTML.length;
556 var unescaped = unlocked.innerHTML.html_to_matita();
557 var parsedtxt = parsed.childNodes[0].nodeValue;
558 //parsedtxt = unescaped.substr(0,len);
559 var unparsedtxt = unescaped.substr(len);
560 lockedbackup += parsedtxt;
561 locked.innerHTML = lockedbackup;
562 unlocked.innerHTML = unparsedtxt.matita_to_html();
563 // len1 = unlocked.innerHTML.length;
564 // len2 = len0 - len1;
565 var len2 = parsedtxt.length;
566 var metasenv = xml.getElementsByTagName("meta");
567 populate_goalarray(metasenv);
568 statements = listcons(len2,statements);
569 unlocked.scrollIntoView(true);
571 else if (is_defined(ambiguity)) {
572 var start = parseInt(ambiguity.getAttribute("start"));
573 var stop = parseInt(ambiguity.getAttribute("stop"));
574 var choices = xml.getElementsByTagName("choice");
576 matita.ambiguityStart = start;
577 matita.ambiguityStop = stop;
578 matita.unlockedbackup = unlocked.innerHTML;
579 matita.interpretations = [];
581 var unlockedtxt = unlocked.innerHTML;
582 var pre = unlockedtxt.substring(0,start);
583 var mid = unlockedtxt.substring(start,stop);
584 var post = unlockedtxt.substring(stop);
585 unlocked.innerHTML = pre +
586 "<span class=\"error\" title=\"disambiguation error\">" +
587 mid + "</span>" + post;
589 var title = "<H3>Ambiguous input</H3>";
590 disambcell.innerHTML = title;
591 for (i = 0;i < choices.length;i++) {
592 matita.interpretations[i] = new Object();
594 var href = choices[i].getAttribute("href");
595 var title = choices[i].getAttribute("title");
596 var desc = choices[i].childNodes[0].nodeValue;
598 matita.interpretations[i].href = href;
599 matita.interpretations[i].title = title;
600 matita.interpretations[i].desc = desc;
602 var choice = document.createElement("input");
603 choice.setAttribute("type","radio");
604 choice.setAttribute("name","interpr");
605 choice.setAttribute("href",href);
606 choice.setAttribute("title",title);
607 if (i == 0) choice.setAttribute("checked","");
609 disambcell.appendChild(choice);
610 disambcell.appendChild(document.createTextNode(desc));
611 disambcell.appendChild(document.createElement("br"));
614 var okbutton = document.createElement("input");
615 okbutton.setAttribute("type","button");
616 okbutton.setAttribute("value","OK");
617 okbutton.setAttribute("onclick","do_disambiguate()");
618 var cancelbutton = document.createElement("input");
619 cancelbutton.setAttribute("type","button");
620 cancelbutton.setAttribute("value","Cancel");
621 cancelbutton.setAttribute("onclick","void(0)");
623 disambcell.appendChild(okbutton);
624 disambcell.appendChild(cancelbutton);
626 matita.disambMode = true;
630 var error = xml.getElementsByTagName("error")[0];
631 unlocked.innerHTML = error.childNodes[0].nodeValue;
632 // debug(xml.childNodes[0].nodeValue);
635 debug("advance failed");
640 callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
644 function gotoBottom()
646 processor = function(xml) {
647 if (is_defined(xml)) {
648 // debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND");
649 parsed = xml.getElementsByTagName("parsed")[0];
650 len = parseInt(parsed.getAttribute("length"));
652 // len0 = unlocked.innerHTML.length;
653 unescaped = unlocked.innerHTML.html_to_matita();
654 // not working in mozilla
655 // parsedtxt = parsed.childNodes[0].nodeValue;
656 parsedtxt = parsed.childNodes[0].wholeText;
657 //parsedtxt = unescaped.substr(0,len);
658 unparsedtxt = unescaped.substr(len);
659 lockedbackup += parsedtxt;
660 locked.innerHTML = lockedbackup; //.matita_to_html();
661 unlocked.innerHTML = unparsedtxt.matita_to_html();
662 // len1 = unlocked.innerHTML.length;
663 len2 = parsedtxt.length;
664 metasenv = xml.getElementsByTagName("meta");
665 populate_goalarray(metasenv);
667 statements = listcons(len2,statements);
668 unlocked.scrollIntoView(true);
671 debug("goto bottom failed");
676 callServer("bottom",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
683 processor = function(xml) {
684 if (is_defined(xml)) {
685 if (xml.childNodes[0].textContent != "ok") {
686 debug("goto top failed");
689 statements = listnil();
691 lockedlen = locked.innerHTML.length - statementlen;
692 statement = locked.innerHTML.substr(lockedlen, statementlen);
693 locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
694 unlocked.innerHTML = statement + unlocked.innerHTML;
696 unlocked.innerHTML = lockedbackup + unlocked.innerHTML;
698 locked.innerHTML = lockedbackup;
700 unlocked.scrollIntoView(true);
702 debug("goto top failed");
707 callServer("top",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
710 function gotoPos(offset)
712 if (!is_defined(offset)) {
713 offset = getCursorPos();
715 processor = function(xml) {
716 if (is_defined(xml)) {
717 parsed = xml.getElementsByTagName("parsed")[0];
718 len = parseInt(parsed.getAttribute("length"));
719 // len0 = unlocked.innerHTML.length;
720 unescaped = unlocked.innerHTML.html_to_matita();
721 parsedtxt = parsed.childNodes[0].nodeValue;
722 //parsedtxt = unescaped.substr(0,len);
723 unparsedtxt = unescaped.substr(len);
724 lockedbackup += parsedtxt;
725 locked.innerHTML = lockedbackup; //.matita_to_html();
726 unlocked.innerHTML = unparsedtxt.matita_to_html();
727 // len1 = unlocked.innerHTML.length;
728 len2 = parsedtxt.length;
729 metasenv = xml.getElementsByTagName("meta");
730 // populate_goalarray(metasenv);
731 statements = listcons(len2,statements);
732 unlocked.scrollIntoView(true);
733 // la populate non andrebbe fatta a ogni passo
735 populate_goalarray(metasenv);
738 gotoPos(offset - len);
741 unlocked.scrollIntoView(true);
742 populate_goalarray(metasenv);
747 callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
752 processor = function(xml) {
753 if (typeof xml != "undefined") {
754 // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
755 statementlen = parseInt(listhd(statements));
756 statements = listtl(statements);
758 lockedlen = locked.innerHTML.length - statementlen;
759 statement = locked.innerHTML.substr(lockedlen, statementlen);
760 locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
761 unlocked.innerHTML = statement + unlocked.innerHTML;
763 lockedlen = lockedbackup.length - statementlen;
764 statement = lockedbackup.substr(lockedlen, statementlen);
765 lockedbackup = lockedbackup.substr(0,lockedlen);
766 locked.innerHTML = lockedbackup;
767 unlocked.innerHTML = statement + unlocked.innerHTML;
768 metasenv = xml.getElementsByTagName("meta");
769 populate_goalarray(metasenv);
770 unlocked.scrollIntoView(true);
772 debug("retract failed");
778 callServer("retract",processor);
784 processor = function(xml)
786 if (is_defined(xml)) {
788 locked.innerHTML = lockedbackup;
789 unlocked.innerHTML = xml.documentElement.wholeText;
791 debug("file open failed");
794 callServer("open",processor,"file=" + escape(filename.value));
797 function retrieveFile(thefile)
799 processor = function(xml)
801 if (is_defined(xml)) {
804 locked.innerHTML = lockedbackup;
805 // code originally used in google chrome (problems with mozilla)
806 // debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
807 // unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
808 debug(xml.childNodes[0].textContent);
809 if (document.all) { // IE
810 unlocked.innerHTML = xml.childNodes[0].text;
812 unlocked.innerHTML = xml.childNodes[0].textContent;
816 debug("file open failed");
819 dialogBox.style.display = "none";
820 callServer("open",processor,"file=" + escape(thefile));
823 function showLibrary(title,callback,reloadDialog)
826 dialogBox.reload = reloadDialog;
828 if (window.XMLHttpRequest)
830 req = new XMLHttpRequest();
832 else if (window.ActiveXObject)
835 req = new ActiveXObject("Msxml2.XMLHTTP");
839 req = new ActiveXObject("Microsoft.XMLHTTP");
843 req.onreadystatechange = function()
851 stxt = req.statusText;
854 debug(req.responseText);
855 showDialog("<H2>" + title + "</H2>",req.responseText, callback);
859 req.open("POST", "viewlib"); // + escape(unlocked.innerHTML), true);
860 req.setRequestHeader("Content-type","application/x-www-form-urlencoded");
865 function uploadDialog()
867 uploadBox.style.display = "block";
872 var file = document.getElementById("uploadFilename").files[0];
874 var filecontent = file.getAsText("UTF-8");
875 locked.innerHTML = lockedbackup;
876 unlocked.innerHTML = filecontent;
877 uploadBox.style.display = "none";
880 // var reader = new FileReader();
881 // reader.readAsText(file, "UTF-8");
882 // reader.onloadend = function (evt) {
883 // lockedbackup = "";
884 // locked.innerHTML = lockedbackup
885 // unlocked.innerHTML = evt.target.result;
886 // uploadBox.style.display = "none";
888 // reader.onerror = function (evt) {
889 // debug("file open failed");
890 // uploadBox.style.display = "none";
895 function openDialog()
897 callback = function (fname) { retrieveFile(fname); };
898 showLibrary("Open file", callback, openDialog);
901 function saveDialog()
903 callback = function (fname) {
904 dialogBox.style.display = "none";
906 (locked.innerHTML.html_to_matita()).sescape(),
907 (unlocked.innerHTML.html_to_matita()).sescape(),
910 showLibrary("Save file as", callback, saveDialog);
915 callback = function (fname) {
916 dialogBox.style.display = "none";
917 saveFile(fname,"","",false,newDialog,true);
919 showLibrary("Create new file", callback, newDialog);
923 function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog,reloadFile)
925 if (!is_defined(reloadFile)) { reloadFile = true };
926 if (!is_defined(fname)) {
927 fname = current_fname;
928 lockedtxt = (locked.innerHTML.html_to_matita()).sescape();
929 unlockedtxt = (unlocked.innerHTML.html_to_matita()).sescape();
931 // when force is true, reloadDialog is not needed
933 processor = function(xml) {
934 if (is_defined(xml)) {
935 if (xml.childNodes[0].textContent != "ok") {
936 if (confirm("File already exists. All existing data will be lost.\nDo you want to proceed anyway?")) {
937 saveFile(fname,lockedtxt,unlockedtxt,true,reloadDialog,reloadFile);
943 debug("file saved!");
944 if (reloadFile) { retrieveFile(fname); }
947 debug("save file failed");
951 if (is_defined(fname)) {
953 callServer("save",processor,"file=" + escape(fname) +
954 "&locked=" + lockedtxt +
955 "&unlocked=" + unlockedtxt +
958 else { debug("no file selected"); }
961 function createDir() {
963 dirname = prompt("New directory name:\ncic:/matita/","newdir");
964 if (dirname != null) {
965 processor = function(xml) {
966 if (is_defined(xml)) {
967 if (xml.childNodes[0].textContent != "ok") {
968 alert("An error occurred :-(");
971 alert("An error occurred :-(");
976 callServer("save",processor,"file=" + escape(dirname) +
977 "&locked=&unlocked=&force=false&dir=true");
985 processor = function(xml) {
986 if (is_defined(xml)) {
987 debug(xml.getElementsByTagName("details")[0].textContent);
988 alert("Commit executed: see details in the log.\n\n" +
989 "NOTICE: this message does NOT imply (yet) that the commit was successful.");
991 alert("Commit failed!");
996 callServer("commit",processor);
1001 processor = function(xml) {
1002 if (is_defined(xml)) {
1003 alert("Update executed.\n\n" +
1005 xml.getElementsByTagName("details")[0].textContent);
1007 alert("Update failed!");
1012 callServer("update",processor);
1017 function hideSequent() {
1018 matita.proofMode = false;
1022 function showSequent() {
1023 matita.proofMode = true;
1027 function showDialog(title,content,callback) {
1028 dialogTitle.innerHTML = title;
1029 dialogContent.innerHTML = content;
1030 dialogBox.callback = callback;
1031 dialogBox.style.display = "block";
1034 function showDisamb(content) {
1035 disambContent.innerHTML = content;
1036 disambBox.style.display = "block";
1039 function abortDialog(dialog) {
1040 dialogBox.style.display = "none";
1043 function removeElement(id) {
1044 var element = document.getElementById(id);
1045 element.parentNode.removeChild(element);
1051 function getCursorPos() {
1053 if (window.getSelection) {
1054 var selObj = window.getSelection();
1055 savedRange = selObj.getRangeAt(0);
1056 savedsc = savedRange.startContainer;
1057 savedso = savedRange.startOffset;
1058 //cursorPos = findNode(selObj.anchorNode.parentNode.childNodes, selObj.anchorNode) + selObj.anchorOffset;
1059 cursorPos = findNode(unlocked.childNodes, selObj.anchorNode,0) + selObj.anchorOffset;
1060 /* FIXME the following works wrong in Opera when the document is longer than 32767 chars */
1063 else if (document.selection) {
1064 savedRange = document.selection.createRange();
1065 var bookmark = savedRange.getBookmark();
1066 /* FIXME the following works wrong when the document is longer than 65535 chars */
1067 cursorPos = bookmark.charCodeAt(2) - 11; /* Undocumented function [3] */
1072 function findNode(list, node, acc) {
1073 for (var i = 0; i < list.length; i++) {
1074 if (list[i] == node) {
1075 // debug("success " + i);
1078 if (list[i].hasChildNodes()) {
1080 // debug("recursion on node " + i);
1081 return (findNode(list[i].childNodes,node,acc))
1083 catch (e) { /* debug("recursion failed"); */ }
1085 sandbox = document.getElementById("sandbox");
1086 dup = list[i].cloneNode(true);
1087 sandbox.appendChild(dup);
1088 // debug("fail " + i + ": " + sandbox.innerHTML);
1089 acc += sandbox.innerHTML.length;
1090 sandbox.removeChild(dup);
1096 debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos()));
1099 function get_checked_index(name) {
1100 var radios = document.getElementsByName(name);
1101 for (i = 0; i < radios.length; i++) {
1102 if (radios[i].checked) {
1109 function do_disambiguate() {
1110 var i = get_checked_index("interpr");
1112 var pre = matita.unlockedbackup.substring(0,matita.ambiguityStart);
1113 var mid = matita.unlockedbackup.substring(matita.ambiguityStart,matita.ambiguityStop);
1114 var post = matita.unlockedbackup.substring(matita.ambiguityStop);
1116 var href = matita.interpretations[i].href;
1117 var title = matita.interpretations[i].title;
1119 if (is_defined(title)) {
1120 mid = "<A href=\"" + href + "\" title=\"" + title + "\">" + mid + "</A>";
1122 mid = "<A href=\"" + href + "\">" + mid + "</A>";
1125 unlocked.innerHTML = pre + mid + post;
1127 matita.disambMode = false;
1132 function readCookie(name) {
1133 var nameEQ = name + "=";
1134 var ca = document.cookie.split(';');
1135 for(var i=0;i < ca.length;i++) {
1137 while (c.charAt(0)==' ') c = c.substring(1,c.length);
1138 if (c.indexOf(nameEQ) == 0) return c.substring(nameEQ.length,c.length);
1143 function delete_cookie ( cookie_name )
1145 var cookie_date = new Date(); // current date & time
1146 cookie_date.setTime ( cookie_date.getTime() - 1 );
1147 document.cookie = cookie_name += "=; expires=" + cookie_date.toGMTString();
1150 function delete_session()
1152 delete_cookie("session");