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,cname){
38 var itemsfound = new Array;
39 for(var i=0;i<elements.length;i++){
40 if(elements[i].className == cname){
41 itemsfound.push(elements[i]);
49 if (readCookie("session") == null) {
50 window.location = "/login.html"
52 matitaLayout = $('body').layout({
53 applyDefaultStyles: true,
59 onresize_end : resizeSide,
61 size: int_of_px($('body').width())/3
70 titlebar = document.getElementById("titlebar");
71 matitaTitle = document.getElementById("matitaTitle");
72 apparea = document.getElementById("matitaapparea");
73 locked = document.getElementById("locked");
74 unlocked = document.getElementById("unlocked");
75 toparea = document.getElementById("toparea");
76 workarea = document.getElementById("workarea");
77 scriptcell = document.getElementById("scriptcell");
78 sidearea = document.getElementById("sidearea");
79 disambcell = document.getElementById("disambcell");
80 goalcell = document.getElementById("goalcell");
81 goals = document.getElementById("goals");
82 goalview = document.getElementById("goalview");
83 filename = document.getElementById("filename");
84 logarea = document.getElementById("logarea");
85 advanceButton = document.getElementById("advance");
86 retractButton = document.getElementById("retract");
87 cursorButton = document.getElementById("cursor");
88 bottomButton = document.getElementById("bottom");
89 dialogBox = document.getElementById("dialogBox");
90 uploadBox = document.getElementById("uploadBox");
91 dialogTitle = document.getElementById("dialogTitle");
92 dialogContent = document.getElementById("dialogContent");
94 matita = new Object();
95 matita.disambMode = matita.proofMode = false;
97 // hide sequent view at start
102 matitaLayout.hide("south");
104 // changeFile("test.ma");
105 retrieveFile("test.ma");
107 // initialize keyboard events in the unlocked script
108 init_keyboard(unlocked);
116 function go_hyperlink(atag) {
117 var uri = atag.attr("href");
118 var mybaseuri = uri.substring(0,uri.lastIndexOf('/'));
119 var id = uri.substring(uri.lastIndexOf('/')+1,uri.lastIndexOf('.'));
120 // only non-notations
121 if (uri != "cic:/fakeuri.def(1)") {
122 if (mybaseuri == baseuri) {
124 $('#'+id)[0].scrollIntoView(true);
126 // best effort: if undefined, don't scroll
129 createDocWin(mybaseuri,id);
135 function init_hyperlinks() {
136 $("#unlocked a").click(function () { return go_hyperlink($(this))});
137 $("#locked a").click(function () { return go_hyperlink($(this))});
138 $("#goalview a").click(function () { return go_hyperlink($(this))});
141 function init_autotraces() {
142 $("#unlocked .autotactic").tooltip({
145 bodyHandler: function() {
146 return (trace_of($(this)[0]));
149 $("#locked .autotactic").tooltip({
152 bodyHandler: function() {
153 return (trace_of($(this)[0]));
158 function trace_of(node) {
159 return text_of_html(filterByClass(node.childNodes,"autotrace")[0]);
162 function changeFile(name) {
163 current_fname = name;
164 matitaTitle.innerHTML = "cic:/matita/" + name;
165 baseuri = "cic:/matita/" + name.substring(0,name.lastIndexOf('.'));
168 function init_keyboard(target)
170 if (target.addEventListener)
172 // target.addEventListener("keydown",keydown,false);
173 target.addEventListener("keypress",keypress,false);
174 // target.addEventListener("keyup",keyup,false);
175 // target.addEventListener("textInput",textinput,false);
177 else if (target.attachEvent)
179 // target.attachEvent("onkeydown", keydown);
180 target.attachEvent("onkeypress", keypress);
181 // target.attachEvent("onkeyup", keyup);
182 // target.attachEvent("ontextInput", textinput);
186 // target.onkeydown= keydown;
187 target.onkeypress= keypress;
188 // target.onkeyup= keyup;
189 // target.ontextinput= textinput; // probably doesn't work
196 if (n == null) return 'undefined';
198 if (n >= 32 && n < 127) s+= ' (' + String.fromCharCode(n) + ')';
199 while (s.length < 9) s+= ' ';
203 function string_of_key(n)
205 if (n == null) return 'undefined';
206 return String.fromCharCode(n);
209 function pressmesg(w,e)
211 /* for debugging only
212 debug(w + ' keyCode=' + keyval(e.keyCode) +
213 ' which=' + keyval(e.which) +
214 ' charCode=' + keyval(e.charCode) +
215 '\n shiftKey='+e.shiftKey
216 + ' ctrlKey='+e.ctrlKey
217 + ' altKey='+e.altKey
218 + ' metaKey='+e.metaKey);
222 function suppressdefault(e,flag)
226 if (e.preventDefault) e.preventDefault();
227 if (e.stopPropagation) e.stopPropagation();
232 function restoreSelection(r) {
235 if (window.getSelection)//non IE and there is already a selection
237 var s = window.getSelection();
238 if (s.rangeCount > 0)
243 if (document.createRange)//non IE and no selection
245 window.getSelection().addRange(r);
248 if (document.selection)//IE
255 function lookup_tex(texmacro)
257 texmacro = texmacro.substring(1);
258 return unescape(macro2utf8[texmacro]);
261 function strip_tags(tagname,classname)
264 if (is_defined(classname)) {
265 tags = $("#unlocked " + tagname + "." + classname);
267 tags = $("#unlocked " + tagname);
269 var tlen = tags.length; // preserving the value from removeChild operations
270 for (i = 0; i < tlen; i++) {
271 var children = tags[i].childNodes;
272 for (j = 0; j < children.length; j++) {
273 tags[i].parentNode.insertBefore(children[j],tags[i]);
280 var tags = unlocked.getElementsByTagName(tagname);
281 if (is_defined(classname)) {
282 tags = filterByClass(tags,classname);
284 var tlen = tags.length; // preserving the value from removeChild operations
285 for (i = 0; i < tlen; i++) {
286 var children = tags[i].childNodes;
287 for (j = 0; j < children.length; j++) {
288 tags[i].parentNode.insertBefore(children[j],tags[i]);
291 for (var i = 0; i < tlen; i++) {
292 tags[0].parentNode.removeChild(tags[0]);
297 function strip_interpr() {
301 // alert("strip_interpr ended");
304 function strip_anchors() {
305 strip_tags("IMG","anchor");
311 pressmesg('keypress',e);
312 var s = string_of_key(e.charCode);
313 strip_tags("span","error");
316 i = unlocked.innerHTML.html_to_matita().lastIndexOf('\\',j);
318 match = unlocked.innerHTML.html_to_matita().substring(i,j);
319 sym = unescape_html(lookup_tex(match));
320 if (sym != "undefined") {
321 if (window.getSelection) { // non IE
322 savedRange.setStart(savedsc,savedso - (j-i));
323 savedRange.deleteContents();
324 savedRange.insertNode(document.createTextNode(sym));
325 savedsc.parentNode.normalize();
326 if (savedRange.collapsed) { // Mozilla
327 savedRange.setEnd(savedsc,savedRange.endOffset + sym.length);
329 savedRange.collapse(false);
331 savedRange.moveStart(i-j);
332 savedRange.text(sym);
333 savedRange.collapse(false);
335 restoreSelection(savedRange);
336 return suppressdefault(e,true);
339 // restoreSelection(0);
340 return suppressdefault(e,false);
343 else return suppressdefault(e,false);
345 return suppressdefault(e,false);
353 // internet explorer (v.9) doesn't work with innerHTML
354 // but google chrome's innerText is, in a sense, "write only"
355 // what should we do?
356 // logarea.innerText = txt + "\n" + logarea.innerText;
357 logtxt = /* logtxt + "\n" +*/ txt;
362 $('#bottomtext').children().first().text(txt);
363 matitaLayout.show("south");
367 var logWin = window.open( "", "Matita Log",
368 "width=600,height=450,location=no,menubar=no,status=no,scrollbars,resizable,screenX=20,screenY=40,left=20,top=40");
369 logWin.document.write('<html><head><title>Matita Log' + '</title></head>');
370 logWin.document.write('<body><textarea style="width:100%;height:100%;">' +
371 logtxt + '</textarea></body></html>');
372 logWin.document.close();
378 debug("hd of '" + l + "' = '" + ar[0] + "'");
386 debug("tl of '" + l + "' = '" + tl + "'");
390 function listcons(x,l)
392 debug("cons '" + x + "' on '" + l + "'");
393 return (x + "#" + l);
401 function list_append(l1,l2)
409 function fold_left (f,acc,l)
412 { debug("'" + l + "' is fold end");
415 { debug("'" + l + "' is fold cons");
416 return(fold_left (f,f(acc,(listhd(l))),listtl(l))); }
419 function listiter (f,l)
422 { debug("'" + l + "' is nil");
427 debug("'" + l + "' is not nil");
429 listiter(f,listtl(l));
433 function listmap (f,l)
435 debug("listmap on " + l);
437 { debug("returning listnil");
441 { debug("cons f(hd) map(f,tl)");
442 return(f(listhd(l)) + "#" + listmap(f,listtl(l)));
446 var statements = listnil();
449 var metalist = listnil();
451 function pairmap (f,p)
453 debug("pairmap of '" + p + "'");
455 return (f(ar[0],ar[1]));
458 function tripletmap (f,p)
460 debug("tripletmap of '" + p + "'");
462 return (f(ar[0],ar[1],ar[2]));
468 return (pairmap (function (a,b) { return (a); }, p));
474 return (tripletmap (function (a,b,c) { return (a); }, p));
480 return (tripletmap (function (a,b,c) { return (b); }, p));
486 return (tripletmap (function (a,b,c) { return (c); }, p));
489 function populate_goalarray(menv)
491 debug("metasenv.length = " + menv.length);
492 if (menv.length == 0) {
498 goalarray = new Array();
499 metalist = listnil();
500 var tmp_goallist = "";
501 for (i = 0; i < menv.length; i++) {
502 metano = menv[i].getAttribute("number");
503 // item 0 = <metaname>, item 1 = <goal>
504 metaname = menv[i].childNodes[0].childNodes[0].wholeText;
505 goal = menv[i].childNodes[1].childNodes[0].wholeText;
506 debug ("found meta n. " + metano);
507 debug ("found goal\nBEGIN" + goal + "\nEND");
508 goalarray[metano] = goal;
509 tmp_goallist = " <A href=\"javascript:switch_goal(" + metano + ")\">" + metaname + "</A>" + tmp_goallist;
510 metalist = listcons(metano,metalist);
511 debug ("goalarray[\"" + metano + "\"] = " + goalarray[metano]);
513 goals.innerHTML = tmp_goallist;
514 debug("new metalist is '" + metalist + "'");
515 if (is_nil(metalist)) {
519 switch_goal(listhd(metalist));
524 function switch_goal(meta)
526 if (typeof meta == "undefined") {
527 goalview.innerHTML = "";
530 debug("switch_goal " + meta + "\n" + goalarray[meta]);
531 goalview.innerHTML = "<B>Goal ?" + meta + ":</B>\n\n" + goalarray[meta];
535 // the following is used to avoid escaping unicode, which results in
536 // the server being unable to unescape the string
537 String.prototype.sescape = function() {
543 result = result.replace(patt1,"%25");
544 result = result.replace(patt2,"%3D");
545 result = result.replace(patt3,"%26");
546 result = result.replace(patt4,"%2B");
550 String.prototype.html_to_matita = function()
552 var patt1 = /<br(\/|)>/gi;
555 var patt4 = /</gi;
556 var patt5 = />/gi;
557 var patt6 = / /gi;
559 result = result.replace(patt1,"\n");
560 result = result.replace(patt2,"\005");
561 result = result.replace(patt3,"\006");
562 result = result.replace(patt4,"<");
563 result = result.replace(patt5,">");
564 result = result.replace(patt6," ");
565 return (unescape(result));
568 String.prototype.matita_to_html = function()
572 var patt3 = /\005/gi;
573 var patt4 = /\006/gi;
575 result = result.replace(patt1,"<");
576 result = result.replace(patt2,">");
577 result = result.replace(patt3,"<");
578 result = result.replace(patt4,">");
579 return (unescape(result));
582 function is_defined(x)
584 return (typeof x != "undefined");
587 /* servicename: name of the service being called
588 * reqbody: text of the request
589 * processResponse: processes the server response
590 * (takes the response text in input, undefined in case of error)
592 function callServer(servicename,processResponse,reqbody)
596 if (window.XMLHttpRequest)
598 req = new XMLHttpRequest();
600 else if (window.ActiveXObject)
603 req = new ActiveXObject("Msxml2.XMLHTTP");
607 req = new ActiveXObject("Microsoft.XMLHTTP");
611 req.onreadystatechange = function()
619 stxt = req.statusText;
622 debug(req.responseText);
623 if (window.DOMParser) {
624 parser=new DOMParser();
625 xmlDoc=parser.parseFromString(req.responseText,"text/xml");
627 else // Internet Explorer
629 xmlDoc=new ActiveXObject("Microsoft.XMLDOM");
630 xmlDoc.async="false";
631 xmlDoc.loadXML(req.responseText);
633 processResponse(xmlDoc);
635 // in case of error, assume session has expired
636 window.location = "/login.html";
637 // processResponse();
641 req.open("POST", servicename); // + escape(unlocked.innerHTML), true);
642 req.setRequestHeader("Content-type","application/x-www-form-urlencoded");
651 function advOneStep(xml) {
652 var parsed = xml.getElementsByTagName("parsed")[0];
653 var ambiguity = xml.getElementsByTagName("ambiguity")[0];
654 var disamberr = xml.getElementsByTagName("disamberror")[0];
655 var localized = xml.getElementsByTagName("localized")[0];
656 if (is_defined(parsed)) {
657 // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
658 var len = parseInt(parsed.getAttribute("length"));
660 // len0 = unlocked.innerHTML.length;
661 var unescaped = unlocked.innerHTML.html_to_matita();
662 var parsedtxt = parsed.childNodes[0].wholeText;
663 //parsedtxt = unescaped.substr(0,len);
664 var unparsedtxt = unescaped.substr(len);
665 lockedbackup += parsedtxt;
666 locked.innerHTML = lockedbackup;
667 unlocked.innerHTML = unparsedtxt.matita_to_html();
668 // len1 = unlocked.innerHTML.length;
669 // len2 = len0 - len1;
670 var len2 = parsedtxt.length;
671 metasenv = xml.getElementsByTagName("meta");
672 statements = listcons(len2,statements);
673 //unlocked.scrollIntoView(true);
678 else if (is_defined(ambiguity)) {
679 var start = parseInt(ambiguity.getAttribute("start"));
680 var stop = parseInt(ambiguity.getAttribute("stop"));
681 var choices = xml.getElementsByTagName("choice");
683 matita.ambiguityStart = start;
684 matita.ambiguityStop = stop;
685 matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
686 matita.interpretations = [];
688 var unlockedtxt = unlocked.innerHTML.html_to_matita();
689 var pre = unlockedtxt.substring(0,start).matita_to_html();
690 var mid = unlockedtxt.substring(start,stop).matita_to_html();
691 var post = unlockedtxt.substring(stop).matita_to_html();
692 unlocked.innerHTML = pre +
693 "<span class=\"error\" title=\"disambiguation error\">" +
694 mid + "</span>" + post;
696 var title = "<H3>Ambiguous input</H3>";
697 disambcell.innerHTML = title;
698 for (i = 0;i < choices.length;i++) {
699 matita.interpretations[i] = new Object();
701 var href = choices[i].getAttribute("href");
702 var title = choices[i].getAttribute("title");
703 var desc = choices[i].childNodes[0].nodeValue;
705 matita.interpretations[i].href = href;
706 matita.interpretations[i].title = title;
707 matita.interpretations[i].desc = desc;
709 var choice = document.createElement("input");
710 choice.setAttribute("type","radio");
711 choice.setAttribute("name","interpr");
712 choice.setAttribute("href",href);
713 choice.setAttribute("title",title);
714 if (i == 0) choice.setAttribute("checked","");
716 disambcell.appendChild(choice);
717 disambcell.appendChild(document.createTextNode(desc));
718 disambcell.appendChild(document.createElement("br"));
721 var okbutton = document.createElement("input");
722 okbutton.setAttribute("type","button");
723 okbutton.setAttribute("value","OK");
724 okbutton.setAttribute("onclick","do_disambiguate()");
725 var cancelbutton = document.createElement("input");
726 cancelbutton.setAttribute("type","button");
727 cancelbutton.setAttribute("value","Cancel");
728 cancelbutton.setAttribute("onclick","cancel_disambiguate()");
730 disambcell.appendChild(okbutton);
731 disambcell.appendChild(cancelbutton);
733 matita.disambMode = true;
737 else if (is_defined(disamberr)) {
738 // must be fixed in a daemon: it makes sense to return a
739 // disambiguation error with no choices
740 if (disamberr.childNodes.length > 0) {
741 set_cps(disamberr.childNodes);
742 matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
743 matita.disambMode = true;
747 } else if (is_defined(localized)) {
748 unlocked.innerHTML = localized.childNodes[0].wholeText;
752 var err = xml.getElementsByTagName("error")[0];
753 error(err.childNodes[0].nodeValue);
759 function advanceForm1()
761 processor = function(xml) {
763 if (is_defined(xml)) {
765 populate_goalarray(metasenv);
769 error("advance failed");
777 callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
781 // get or set <choicepoint>'s (in case of disamb error)
783 return matita.choicepoints
786 function set_cps(cps) {
787 matita.choicepoints = cps;
790 // get radio buttons for <choice>'s in a given cp
791 function get_choice_opts(i) {
793 var choices = get_cps()[i].childNodes;
794 for (var j = 0;j < choices.length;j++) {
795 var href = choices[j].getAttribute("href");
796 var title = choices[j].getAttribute("title");
798 if (is_defined(title) && title != null) {
800 } else if (is_defined(href) && href != null) {
806 res[j] = document.createElement("input");
807 res[j].setAttribute("type","radio");
808 res[j].setAttribute("name","choice");
809 res[j].setAttribute("choicepointno",i);
810 res[j].setAttribute("choiceno",j);
811 res[j].setAttribute("href",href);
812 res[j].setAttribute("title",title);
813 if (desc != null) res[j].setAttribute("desc",desc);
815 if (j == 0) res[j].setAttribute("checked","");
820 // get radio buttons for <failure>'s in a given choice
821 function get_failure_opts(i,j) {
823 var failures = get_cps()[i].childNodes[j].childNodes;
824 for (var k = 0;k < failures.length;k++) {
825 var start = failures[k].getAttribute("start");
826 var stop = failures[k].getAttribute("stop");
827 var title = failures[k].getAttribute("title");
829 res[k] = document.createElement("input");
830 res[k].setAttribute("type","radio");
831 res[k].setAttribute("name","failure");
832 res[k].setAttribute("choicepointno",i);
833 res[k].setAttribute("choiceno",j);
834 res[k].setAttribute("failureno",k);
835 res[k].setAttribute("start",start);
836 res[k].setAttribute("stop",stop);
837 res[k].setAttribute("title",title);
839 if (k == 0) res[k].setAttribute("checked","");
844 function next_cp(curcp) {
845 var cp = get_cps()[curcp];
846 var start = parseInt(cp.getAttribute("start"));
847 var stop = parseInt(cp.getAttribute("stop"));
849 matita.errorStart = start;
850 matita.errorStop = stop;
851 // matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
853 var unlockedtxt = matita.unlockedbackup;
854 var pre = unlockedtxt.substring(0,start).matita_to_html();
855 var mid = unlockedtxt.substring(start,stop).matita_to_html();
856 var post = unlockedtxt.substring(stop).matita_to_html();
857 unlocked.innerHTML = pre +
858 "<span class=\"error\" title=\"error location\">" +
859 mid + "</span>" + post;
861 var title = "<H3>Error diagnostics</H3>";
862 disambcell.innerHTML = title;
863 var choices = get_choice_opts(curcp);
864 for (var i = 0;i < choices.length;i++) {
865 disambcell.appendChild(choices[i]);
866 var desc = choices[i].getAttribute("desc");
867 if (!is_defined(desc) || desc == null) {
868 desc = "Interpretation " + i;
870 disambcell.appendChild(document.createTextNode(desc));
871 disambcell.appendChild(document.createElement("br"));
874 // update index of the next choicepoint
875 new_curcp = (curcp + 1) % get_cps().length;
877 var okbutton = document.createElement("input");
878 okbutton.setAttribute("type","button");
879 okbutton.setAttribute("value","OK");
880 okbutton.setAttribute("onclick","show_failures()");
881 var cancelbutton = document.createElement("input");
882 cancelbutton.setAttribute("type","button");
883 cancelbutton.setAttribute("value","Close");
884 cancelbutton.setAttribute("onclick","cancel_disambiguate()");
885 var tryagainbutton = document.createElement("input");
886 tryagainbutton.setAttribute("type","button");
888 tryagainbutton.setAttribute("value","Try something else");
890 tryagainbutton.setAttribute("value","Restart");
892 tryagainbutton.setAttribute("onclick","next_cp(" + new_curcp + ")");
894 disambcell.appendChild(okbutton);
895 disambcell.appendChild(tryagainbutton);
896 disambcell.appendChild(cancelbutton);
900 //matita.disambMode = true;
905 function show_failures() {
907 var choice = document.getElementsByName("choice")[get_checked_index("choice")];
908 var cpno = parseInt(choice.getAttribute("choicepointno"));
909 var choiceno = parseInt(choice.getAttribute("choiceno"));
910 var choicedesc = choice.getAttribute("desc");
912 var title = "<H3>Error diagnostics</H3>";
914 if (is_defined(choicedesc) && choicedesc != null) {
915 subtitle = "<p>Errors at node " + cpno + " = " + choicedesc + "</p>";
917 subtitle = "<p>Global errors:</p>";
920 disambcell.innerHTML = title + subtitle;
921 var failures = get_failure_opts(cpno,choiceno);
922 for (var i = 0;i < failures.length;i++) {
923 disambcell.appendChild(failures[i]);
924 disambcell.appendChild(document.createTextNode(failures[i].getAttribute("title")));
925 disambcell.appendChild(document.createElement("br"));
928 var okbutton = document.createElement("input");
929 okbutton.setAttribute("type","button");
930 okbutton.setAttribute("value","Show error loc");
931 okbutton.setAttribute("onclick","show_err()");
932 var cancelbutton = document.createElement("input");
933 cancelbutton.setAttribute("type","button");
934 cancelbutton.setAttribute("value","Close");
935 cancelbutton.setAttribute("onclick","cancel_disambiguate()");
936 var backbutton = document.createElement("input");
937 backbutton.setAttribute("type","button");
938 backbutton.setAttribute("value","<< Back");
939 backbutton.setAttribute("onclick","next_cp(" + cpno + ")");
941 disambcell.appendChild(backbutton);
942 disambcell.appendChild(okbutton);
943 disambcell.appendChild(cancelbutton);
947 function show_err() {
948 var radios = document.getElementsByName("failure");
949 for (i = 0; i < radios.length; i++) {
950 if (radios[i].checked) {
951 var start = radios[i].getAttribute("start");
952 var stop = radios[i].getAttribute("stop");
953 var title = radios[i].getAttribute("title");
954 var unlockedtxt = matita.unlockedbackup;
955 var pre = unlockedtxt.substring(0,start).matita_to_html();
956 var mid = unlockedtxt.substring(start,stop).matita_to_html();
957 var post = unlockedtxt.substring(stop).matita_to_html();
958 unlocked.innerHTML = pre +
959 "<span class=\"error\" title=\"Disambiguation failure\">" +
960 mid + "</span>" + post;
966 function gotoBottom()
968 processor = function(xml) {
969 if (is_defined(xml)) {
970 // debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND");
971 var parsed = xml.getElementsByTagName("parsed");
972 var localized = xml.getElementsByTagName("localized")[0];
973 var ambiguity = xml.getElementsByTagName("ambiguity")[0];
974 var generic_err = xml.getElementsByTagName("error")[0];
975 var disamberr = xml.getElementsByTagName("disamberror")[0];
976 for (var i = 0;i < parsed.length; i++) {
977 var len = parsed[i].getAttribute("length");
978 // len0 = unlocked.innerHTML.length;
979 var unescaped = unlocked.innerHTML.html_to_matita();
980 // the browser may decide to split textnodes: use wholeText!
981 var parsedtxt = parsed[i].childNodes[0].wholeText;
982 //parsedtxt = unescaped.substr(0,len);
983 var unparsedtxt = unescaped.substr(len);
984 lockedbackup += parsedtxt;
985 locked.innerHTML = lockedbackup; //.matita_to_html();
986 unlocked.innerHTML = unparsedtxt.matita_to_html();
987 // len1 = unlocked.innerHTML.length;
988 var len2 = parsedtxt.length;
989 statements = listcons(len2,statements);
991 // unlocked.scrollIntoView(true);
993 metasenv = xml.getElementsByTagName("meta");
996 populate_goalarray(metasenv);
998 if (is_defined(ambiguity)) {
999 var start = parseInt(ambiguity.getAttribute("start"));
1000 var stop = parseInt(ambiguity.getAttribute("stop"));
1001 var choices = xml.getElementsByTagName("choice");
1003 matita.ambiguityStart = start;
1004 matita.ambiguityStop = stop;
1005 matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
1006 matita.interpretations = [];
1008 var unlockedtxt = unlocked.innerHTML.html_to_matita();
1009 var pre = unlockedtxt.substring(0,start).matita_to_html();
1010 var mid = unlockedtxt.substring(start,stop).matita_to_html();
1011 var post = unlockedtxt.substring(stop).matita_to_html();
1012 unlocked.innerHTML = pre +
1013 "<span class=\"error\" title=\"disambiguation error\">" +
1014 mid + "</span>" + post;
1016 var title = "<H3>Ambiguous input</H3>";
1017 disambcell.innerHTML = title;
1018 for (i = 0;i < choices.length;i++) {
1019 matita.interpretations[i] = new Object();
1021 var href = choices[i].getAttribute("href");
1022 var title = choices[i].getAttribute("title");
1023 var desc = choices[i].childNodes[0].nodeValue;
1025 matita.interpretations[i].href = href;
1026 matita.interpretations[i].title = title;
1027 matita.interpretations[i].desc = desc;
1029 var choice = document.createElement("input");
1030 choice.setAttribute("type","radio");
1031 choice.setAttribute("name","interpr");
1032 choice.setAttribute("href",href);
1033 choice.setAttribute("title",title);
1034 if (i == 0) choice.setAttribute("checked","");
1036 disambcell.appendChild(choice);
1037 disambcell.appendChild(document.createTextNode(desc));
1038 disambcell.appendChild(document.createElement("br"));
1041 var okbutton = document.createElement("input");
1042 okbutton.setAttribute("type","button");
1043 okbutton.setAttribute("value","OK");
1044 okbutton.setAttribute("onclick","do_disambiguate()");
1045 var cancelbutton = document.createElement("input");
1046 cancelbutton.setAttribute("type","button");
1047 cancelbutton.setAttribute("value","Cancel");
1048 cancelbutton.setAttribute("onclick","cancel_disambiguate()");
1050 disambcell.appendChild(okbutton);
1051 disambcell.appendChild(cancelbutton);
1053 matita.disambMode = true;
1056 else if (is_defined(disamberr)) {
1057 // must be fixed in a daemon: it makes sense to return a
1058 // disambiguation error with no choices
1059 if (disamberr.childNodes.length > 0) {
1060 set_cps(disamberr.childNodes);
1061 matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
1062 matita.disambMode = true;
1067 else if (is_defined(localized)) {
1068 unlocked.innerHTML = localized.childNodes[0].wholeText;
1070 else if (is_defined(generic_err)) {
1071 error("Unmanaged error:\n" + generic_err.childNodes[0].wholeText);
1074 error("goto bottom failed");
1079 callServer("bottom",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
1085 processor = function(xml) {
1086 if (is_defined(xml)) {
1087 if (xml.childNodes[0].textContent != "ok") {
1088 error("goto top failed");
1091 statements = listnil();
1093 lockedlen = locked.innerHTML.length - statementlen;
1094 statement = locked.innerHTML.substr(lockedlen, statementlen);
1095 locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
1096 unlocked.innerHTML = statement + unlocked.innerHTML;
1098 unlocked.innerHTML = lockedbackup + unlocked.innerHTML;
1100 locked.innerHTML = lockedbackup;
1105 // unlocked.scrollIntoView(true);
1108 error("goto top failed");
1113 callServer("top",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
1117 function gotoPos(offset)
1119 if (!is_defined(offset)) {
1120 offset = getCursorPos();
1122 processor = function(xml) {
1123 if (is_defined(xml)) {
1125 var len = advOneStep(xml);
1126 if (len == 0 || offset <= len) {
1129 populate_goalarray(metasenv);
1132 gotoPos(offset - len);
1137 populate_goalarray(metasenv);
1143 // unlocked.scrollIntoView(true);
1145 populate_goalarray(metasenv);
1150 callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
1153 function retractStep()
1155 if (!is_nil(statements)) {
1156 processor = function(xml) {
1157 if (typeof xml != "undefined") {
1158 // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
1159 statementlen = parseInt(listhd(statements));
1160 statements = listtl(statements);
1162 lockedlen = locked.innerHTML.length - statementlen;
1163 statement = locked.innerHTML.substr(lockedlen, statementlen);
1164 locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
1165 unlocked.innerHTML = statement + unlocked.innerHTML;
1167 lockedlen = lockedbackup.length - statementlen;
1168 statement = lockedbackup.substr(lockedlen, statementlen);
1169 lockedbackup = lockedbackup.substr(0,lockedlen);
1170 locked.innerHTML = lockedbackup;
1171 unlocked.innerHTML = statement + unlocked.innerHTML;
1172 metasenv = xml.getElementsByTagName("meta");
1173 populate_goalarray(metasenv);
1177 // unlocked.scrollIntoView(true);
1180 error("retract failed");
1185 callServer("retract",processor);
1191 processor = function(xml)
1193 if (is_defined(xml)) {
1195 locked.innerHTML = lockedbackup;
1196 unlocked.innerHTML = xml.documentElement.wholeText;
1199 error("file open failed");
1202 callServer("open",processor,"file=" + escape(filename.value));
1205 function retrieveFile(thefile)
1207 processor = function(xml)
1209 if (is_defined(xml)) {
1210 if (!is_defined(xml.getElementsByTagName("error")[0])) {
1211 changeFile(thefile);
1212 matita.disambMode = false;
1213 matita.proofMode = false;
1216 locked.innerHTML = lockedbackup;
1217 // code originally used in google chrome (problems with mozilla)
1218 // debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
1219 // unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
1220 debug(xml.childNodes[0].textContent);
1221 if (document.all) { // IE
1222 unlocked.innerHTML = xml.childNodes[0].text;
1224 unlocked.innerHTML = xml.childNodes[0].textContent;
1229 unlocked.scrollIntoView(true);
1231 error("file open failed");
1234 window.location = "/login.html";
1237 abortDialog("dialogBox");
1238 callServer("open",processor,"file=" + escape(thefile));
1241 function go_external_hyperlink(uri,thefile,id)
1243 processor = function(xml)
1245 if (is_defined(xml)) {
1246 // code originally used in google chrome (problems with mozilla)
1247 // debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
1248 // unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
1249 // debug(xml.childNodes[0].textContent);
1251 if (document.all) { // IE
1252 doctext = xml.childNodes[0].text;
1254 doctext= xml.childNodes[0].textContent;
1256 $('#locked').html(doctext);
1258 // scroll to anchor (if it exists)
1259 $('#' + id).get(0).scrollIntoView(true);
1264 $('#locked').html("404 object not found");
1267 callServer("open",processor,"file=" + escape(thefile) + "&readonly=true");
1270 function createDocWin(uri,id) {
1271 // 12 = position of the second '/' in uri (to strip off "cic:/matita/")
1272 var thefile = uri.substring(12) + ".ma";
1273 var title = "Matita Browser - " + uri;
1274 var docWin = window.open( "", "matitabrowser",
1275 "width=800,height=600,location=no,menubar=no,status=no,scrollbars,resizable,screenX=20,screenY=40,left=20,top=40");
1276 docWin.document.write('<html><head><title>' + title + '</title>' +
1277 '<script type="text/javascript" src="jquery.js"></script>' +
1278 '<script type="text/javascript" src="jquery.tooltip.min.js"></script>' +
1279 '<script type="text/javascript" src="matitaweb.js"></script>' +
1280 '<script type="text/javascript">go_external_hyperlink("' + uri + '","' + thefile + '","' + id + '");</script>' +
1281 '<link rel="stylesheet" type="text/css" href="matitaweb.css"/>' +
1282 '<link rel="stylesheet" type="text/css" href="jquery.tooltip.css"/>' +
1284 docWin.document.write('<body><H1>'+ uri + '</H1>' +
1285 '<pre id="locked"></pre></body></html>');
1286 docWin.document.close();
1287 docWin.baseuri = uri;
1291 function showLibrary(title,callback,reloadDialog)
1294 dialogBox.reload = reloadDialog;
1296 if (window.XMLHttpRequest)
1298 req = new XMLHttpRequest();
1300 else if (window.ActiveXObject)
1303 req = new ActiveXObject("Msxml2.XMLHTTP");
1307 req = new ActiveXObject("Microsoft.XMLHTTP");
1311 req.onreadystatechange = function()
1314 rs = req.readyState;
1319 stxt = req.statusText;
1322 debug(req.responseText);
1323 showDialog("<H2>" + title + "</H2>",req.responseText, callback);
1327 req.open("POST", "viewlib"); // + escape(unlocked.innerHTML), true);
1328 req.setRequestHeader("Content-type","application/x-www-form-urlencoded");
1333 function uploadDialog()
1335 uploadBox.style.display = "block";
1340 var file = document.getElementById("uploadFilename").files[0];
1342 // var filecontent = file.getAsText("UTF-8");
1343 // locked.innerHTML = lockedbackup;
1344 // unlocked.innerHTML = filecontent;
1345 // uploadBox.style.display = "none";
1348 var reader = new FileReader();
1349 reader.onerror = function (evt) {
1350 error("file open failed");
1352 reader.onload = function (evt) {
1354 locked.innerHTML = lockedbackup
1355 unlocked.innerHTML = "";
1356 unlocked.appendChild(document.createTextNode(evt.target.result));
1357 uploadBox.style.display = "none";
1359 try { reader.readAsText(file, "UTF-8"); }
1360 catch (err) { /* nothing to do */ };
1361 uploadBox.style.display = "none";
1365 function openDialog()
1367 callback = function (fname) { retrieveFile(fname); };
1368 showLibrary("Open file", callback, openDialog);
1371 function saveDialog()
1373 callback = function (fname) {
1374 abortDialog("dialogBox");
1376 (locked.innerHTML.html_to_matita()).sescape(),
1377 (unlocked.innerHTML.html_to_matita()).sescape(),
1380 showLibrary("Save file as", callback, saveDialog);
1383 function newDialog()
1385 callback = function (fname) {
1386 abortDialog("dialogBox");
1389 false,newDialog,true);
1391 showLibrary("Create new file", callback, newDialog);
1395 function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog,reloadFile)
1397 if (!is_defined(reloadFile)) { reloadFile = true };
1398 if (!is_defined(fname)) {
1399 fname = current_fname;
1400 lockedtxt = (locked.innerHTML.html_to_matita()).sescape();
1401 unlockedtxt = (unlocked.innerHTML.html_to_matita()).sescape();
1403 // when force is true, reloadDialog is not needed
1405 processor = function(xml) {
1406 if (is_defined(xml)) {
1407 if (xml.childNodes[0].textContent != "ok") {
1408 if (confirm("File already exists. All existing data will be lost.\nDo you want to proceed anyway?")) {
1409 saveFile(fname,lockedtxt,unlockedtxt,true,reloadDialog,reloadFile);
1415 debug("file saved!");
1416 if (reloadFile) { retrieveFile(fname); }
1419 error("save file failed");
1423 if (is_defined(fname)) {
1425 callServer("save",processor,"file=" + escape(fname) +
1426 "&locked=" + lockedtxt +
1427 "&unlocked=" + unlockedtxt +
1430 else { error("no file selected"); }
1433 function createDir() {
1434 abortDialog("dialogBox");
1435 dirname = prompt("New directory name:\ncic:/matita/","newdir");
1436 if (dirname != null) {
1437 processor = function(xml) {
1438 if (is_defined(xml)) {
1439 if (xml.childNodes[0].textContent != "ok") {
1440 alert("An error occurred :-(");
1443 alert("An error occurred :-(");
1449 callServer("save",processor,"file=" + escape(dirname) +
1450 "&locked=&unlocked=&force=false&dir=true");
1456 function commitAll()
1458 processor = function(xml) {
1459 if (xml.getElementsByTagName("details").length > 0) {
1460 debug(xml.getElementsByTagName("details")[0].textContent);
1461 alert("Commit executed: see details in the log.\n\n" +
1462 "NOTICE: this message does NOT imply (yet) that the commit was successful.");
1464 alert("Commit denied.\nPermission to commit and update is provided by the Matita team upon request.");
1469 callServer("commit",processor);
1472 function updateAll()
1474 processor = function(xml) {
1475 if (xml.getElementsByTagName("details").length > 0) {
1476 alert("Update executed.\n\n" +
1478 xml.getElementsByTagName("details")[0].textContent);
1480 alert("Update denied.\nPermission to commit and update is provided by the Matita team upon request.");
1485 callServer("update",processor);
1490 function hideSequent() {
1491 matita.proofMode = false;
1495 function showSequent() {
1496 matita.proofMode = true;
1500 function showDialog(title,content,callback) {
1501 dialogTitle.innerHTML = title;
1502 dialogContent.innerHTML = content;
1503 dialogBox.callback = callback;
1505 //Get the screen height and width
1506 var maskHeight = $(document).height();
1507 var maskWidth = $(window).width();
1509 //Set heigth and width to mask to fill up the whole screen
1510 $('#mask').css({'width':maskWidth,'height':maskHeight});
1513 $('#mask').fadeIn(100);
1514 $('#mask').fadeTo(200,0.8);
1516 //Get the window height and width
1517 var winH = $(window).height();
1518 var winW = $(window).width();
1520 //Set the popup window to center
1521 $('#dialogBox').css('top', winH/2-$('#dialogBox').height()/2);
1522 $('#dialogBox').css('left', winW/2-$('#dialogBox').width()/2);
1525 $('#dialogBox').fadeIn(200);
1527 dialogBox.style.display = "block";
1530 function abortDialog(dialog) {
1531 document.getElementById(dialog).style.display = "none";
1535 function removeElement(id) {
1536 var element = document.getElementById(id);
1537 element.parentNode.removeChild(element);
1543 function getCursorPos() {
1545 if (window.getSelection) {
1546 var selObj = window.getSelection();
1547 savedRange = selObj.getRangeAt(0);
1548 savedsc = savedRange.startContainer;
1549 savedso = savedRange.startOffset;
1550 //cursorPos = findNode(selObj.anchorNode.parentNode.childNodes, selObj.anchorNode) + selObj.anchorOffset;
1551 cursorPos = findNode(unlocked.childNodes, selObj.anchorNode,0) + selObj.anchorOffset;
1552 /* FIXME the following works wrong in Opera when the document is longer than 32767 chars */
1555 else if (document.selection) {
1556 savedRange = document.selection.createRange();
1557 var bookmark = savedRange.getBookmark();
1558 /* FIXME the following works wrong when the document is longer than 65535 chars */
1559 cursorPos = bookmark.charCodeAt(2) - 11; /* Undocumented function [3] */
1564 function findNode(list, node, acc) {
1565 for (var i = 0; i < list.length; i++) {
1566 if (list[i] == node) {
1567 // debug("success " + i);
1570 if (list[i].hasChildNodes()) {
1572 // debug("recursion on node " + i);
1573 return (findNode(list[i].childNodes,node,acc))
1575 catch (e) { /* debug("recursion failed"); */ }
1577 sandbox = document.getElementById("sandbox");
1578 dup = list[i].cloneNode(true);
1579 sandbox.appendChild(dup);
1580 // debug("fail " + i + ": " + sandbox.innerHTML);
1581 acc += sandbox.innerHTML.html_to_matita().length;
1582 sandbox.removeChild(dup);
1588 debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos()));
1591 function get_checked_index(name) {
1592 var radios = document.getElementsByName(name);
1593 for (i = 0; i < radios.length; i++) {
1594 if (radios[i].checked) {
1601 function cancel_disambiguate() {
1602 matita.disambMode = false;
1604 // enable_toparea();
1605 // enable_editing();
1606 strip_tags("span","error");
1610 function do_disambiguate() {
1611 var i = get_checked_index("interpr");
1613 var pre = matita.unlockedbackup
1614 .substring(0,matita.ambiguityStart).matita_to_html();
1615 var mid = matita.unlockedbackup
1616 .substring(matita.ambiguityStart,matita.ambiguityStop)
1618 var post = matita.unlockedbackup
1619 .substring(matita.ambiguityStop).matita_to_html();
1621 var href = matita.interpretations[i].href;
1622 var title = matita.interpretations[i].title;
1624 if (is_defined(title)) {
1625 mid = "<A href=\"" + href + "\" title=\"" + title + "\">" + mid + "</A>";
1627 mid = "<A href=\"" + href + "\">" + mid + "</A>";
1630 unlocked.innerHTML = pre + mid + post;
1632 matita.disambMode = false;
1639 function do_showerror() {
1640 var i = get_checked_index("choice");
1642 var pre = matita.unlockedbackup
1643 .substring(0,matita.ambiguityStart).matita_to_html();
1644 var mid = matita.unlockedbackup
1645 .substring(matita.ambiguityStart,matita.ambiguityStop)
1647 var post = matita.unlockedbackup
1648 .substring(matita.ambiguityStop).matita_to_html();
1650 var href = matita.interpretations[i].href;
1651 var title = matita.interpretations[i].title;
1653 if (is_defined(title)) {
1654 mid = "<A href=\"" + href + "\" title=\"" + title + "\">" + mid + "</A>";
1656 mid = "<A href=\"" + href + "\">" + mid + "</A>";
1659 unlocked.innerHTML = pre + mid + post;
1664 function readCookie(name) {
1665 var nameEQ = name + "=";
1666 var ca = document.cookie.split(';');
1667 for(var i=0;i < ca.length;i++) {
1669 while (c.charAt(0)==' ') c = c.substring(1,c.length);
1670 if (c.indexOf(nameEQ) == 0) return c.substring(nameEQ.length,c.length);
1675 function delete_cookie ( cookie_name )
1677 var cookie_date = new Date(); // current date & time
1678 cookie_date.setTime ( cookie_date.getTime() - 1 );
1679 document.cookie = cookie_name += "=; expires=" + cookie_date.toGMTString();
1682 function delete_session()
1684 delete_cookie("session");
1687 function disable_toparea() {
1688 var offset = $('#toparea').offset();
1689 $('#whitemask').css('top',offset.top);
1690 $('#whitemask').css('left',offset.left);
1691 $('#whitemask').css('width',$('#toparea').outerWidth() + "px");
1692 $('#whitemask').css('height',$('#toparea').outerHeight() + "px");
1693 $('#whitemask').fadeTo('fast',0.7);
1696 function enable_toparea() {
1697 $('#whitemask').hide();
1700 function disable_editing() {
1701 unlocked.contentEditable = false;
1704 function enable_editing() {
1705 unlocked.contentEditable = true;
1710 // advanceButton.disabled = true;
1711 // retractButton.disabled = true;
1712 // cursorButton.disabled = true;
1713 // bottomButton.disabled = true;
1720 // advanceButton.disabled = false;
1721 // retractButton.disabled = false;
1722 // cursorButton.disabled = false;
1723 // bottomButton.disabled = false;
1724 if (!matita.disambMode) {