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 = "Matita - 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 = $(tagname + "." + classname);
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("INPUT","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 if (is_defined(parsed)) {
656 // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
657 var len = parseInt(parsed.getAttribute("length"));
658 // len0 = unlocked.innerHTML.length;
659 var unescaped = unlocked.innerHTML.html_to_matita();
660 var parsedtxt = parsed.childNodes[0].wholeText;
661 //parsedtxt = unescaped.substr(0,len);
662 var unparsedtxt = unescaped.substr(len);
663 lockedbackup += parsedtxt;
664 locked.innerHTML = lockedbackup;
665 unlocked.innerHTML = unparsedtxt.matita_to_html();
666 // len1 = unlocked.innerHTML.length;
667 // len2 = len0 - len1;
668 var len2 = parsedtxt.length;
669 metasenv = xml.getElementsByTagName("meta");
670 statements = listcons(len2,statements);
671 //unlocked.scrollIntoView(true);
675 else if (is_defined(ambiguity)) {
676 var start = parseInt(ambiguity.getAttribute("start"));
677 var stop = parseInt(ambiguity.getAttribute("stop"));
678 var choices = xml.getElementsByTagName("choice");
680 matita.ambiguityStart = start;
681 matita.ambiguityStop = stop;
682 matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
683 matita.interpretations = [];
685 var unlockedtxt = unlocked.innerHTML.html_to_matita();
686 var pre = unlockedtxt.substring(0,start).matita_to_html();
687 var mid = unlockedtxt.substring(start,stop).matita_to_html();
688 var post = unlockedtxt.substring(stop).matita_to_html();
689 unlocked.innerHTML = pre +
690 "<span class=\"error\" title=\"disambiguation error\">" +
691 mid + "</span>" + post;
693 var title = "<H3>Ambiguous input</H3>";
694 disambcell.innerHTML = title;
695 for (i = 0;i < choices.length;i++) {
696 matita.interpretations[i] = new Object();
698 var href = choices[i].getAttribute("href");
699 var title = choices[i].getAttribute("title");
700 var desc = choices[i].childNodes[0].nodeValue;
702 matita.interpretations[i].href = href;
703 matita.interpretations[i].title = title;
704 matita.interpretations[i].desc = desc;
706 var choice = document.createElement("input");
707 choice.setAttribute("type","radio");
708 choice.setAttribute("name","interpr");
709 choice.setAttribute("href",href);
710 choice.setAttribute("title",title);
711 if (i == 0) choice.setAttribute("checked","");
713 disambcell.appendChild(choice);
714 disambcell.appendChild(document.createTextNode(desc));
715 disambcell.appendChild(document.createElement("br"));
718 var okbutton = document.createElement("input");
719 okbutton.setAttribute("type","button");
720 okbutton.setAttribute("value","OK");
721 okbutton.setAttribute("onclick","do_disambiguate()");
722 var cancelbutton = document.createElement("input");
723 cancelbutton.setAttribute("type","button");
724 cancelbutton.setAttribute("value","Cancel");
725 cancelbutton.setAttribute("onclick","cancel_disambiguate()");
727 disambcell.appendChild(okbutton);
728 disambcell.appendChild(cancelbutton);
730 matita.disambMode = true;
734 else if (is_defined(disamberr)) {
735 // must be fixed in a daemon: it makes sense to return a
736 // disambiguation error with no choices
737 if (disamberr.childNodes.length > 0) {
738 set_cps(disamberr.childNodes);
739 matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
740 matita.disambMode = true;
746 var error = xml.getElementsByTagName("error")[0];
747 unlocked.innerHTML = error.childNodes[0].wholeText;
748 error(xml.childNodes[0].nodeValue);
754 function advanceForm1()
756 processor = function(xml) {
758 if (is_defined(xml)) {
760 populate_goalarray(metasenv);
764 error("advance failed");
772 callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
776 // get or set <choicepoint>'s (in case of disamb error)
778 return matita.choicepoints
781 function set_cps(cps) {
782 matita.choicepoints = cps;
785 // get radio buttons for <choice>'s in a given cp
786 function get_choice_opts(i) {
788 var choices = get_cps()[i].childNodes;
789 for (var j = 0;j < choices.length;j++) {
790 var href = choices[j].getAttribute("href");
791 var title = choices[j].getAttribute("title");
793 if (is_defined(title) && title != null) {
795 } else if (is_defined(href) && href != null) {
801 res[j] = document.createElement("input");
802 res[j].setAttribute("type","radio");
803 res[j].setAttribute("name","choice");
804 res[j].setAttribute("choicepointno",i);
805 res[j].setAttribute("choiceno",j);
806 res[j].setAttribute("href",href);
807 res[j].setAttribute("title",title);
808 if (desc != null) res[j].setAttribute("desc",desc);
810 if (j == 0) res[j].setAttribute("checked","");
815 // get radio buttons for <failure>'s in a given choice
816 function get_failure_opts(i,j) {
818 var failures = get_cps()[i].childNodes[j].childNodes;
819 for (var k = 0;k < failures.length;k++) {
820 var start = failures[k].getAttribute("start");
821 var stop = failures[k].getAttribute("stop");
822 var title = failures[k].getAttribute("title");
824 res[k] = document.createElement("input");
825 res[k].setAttribute("type","radio");
826 res[k].setAttribute("name","failure");
827 res[k].setAttribute("choicepointno",i);
828 res[k].setAttribute("choiceno",j);
829 res[k].setAttribute("failureno",k);
830 res[k].setAttribute("start",start);
831 res[k].setAttribute("stop",stop);
832 res[k].setAttribute("title",title);
834 if (k == 0) res[k].setAttribute("checked","");
839 function next_cp(curcp) {
840 var cp = get_cps()[curcp];
841 var start = parseInt(cp.getAttribute("start"));
842 var stop = parseInt(cp.getAttribute("stop"));
844 matita.errorStart = start;
845 matita.errorStop = stop;
846 // matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
848 var unlockedtxt = matita.unlockedbackup;
849 var pre = unlockedtxt.substring(0,start).matita_to_html();
850 var mid = unlockedtxt.substring(start,stop).matita_to_html();
851 var post = unlockedtxt.substring(stop).matita_to_html();
852 unlocked.innerHTML = pre +
853 "<span class=\"error\" title=\"error location\">" +
854 mid + "</span>" + post;
856 var title = "<H3>Error diagnostics</H3>";
857 disambcell.innerHTML = title;
858 var choices = get_choice_opts(curcp);
859 for (var i = 0;i < choices.length;i++) {
860 disambcell.appendChild(choices[i]);
861 var desc = choices[i].getAttribute("desc");
862 if (!is_defined(desc) || desc == null) {
863 desc = "Interpretation " + i;
865 disambcell.appendChild(document.createTextNode(desc));
866 disambcell.appendChild(document.createElement("br"));
869 // update index of the next choicepoint
870 new_curcp = (curcp + 1) % get_cps().length;
872 var okbutton = document.createElement("input");
873 okbutton.setAttribute("type","button");
874 okbutton.setAttribute("value","OK");
875 okbutton.setAttribute("onclick","show_failures()");
876 var cancelbutton = document.createElement("input");
877 cancelbutton.setAttribute("type","button");
878 cancelbutton.setAttribute("value","Close");
879 cancelbutton.setAttribute("onclick","cancel_disambiguate()");
880 var tryagainbutton = document.createElement("input");
881 tryagainbutton.setAttribute("type","button");
883 tryagainbutton.setAttribute("value","Try something else");
885 tryagainbutton.setAttribute("value","Restart");
887 tryagainbutton.setAttribute("onclick","next_cp(" + new_curcp + ")");
889 disambcell.appendChild(okbutton);
890 disambcell.appendChild(tryagainbutton);
891 disambcell.appendChild(cancelbutton);
895 //matita.disambMode = true;
900 function show_failures() {
902 var choice = document.getElementsByName("choice")[get_checked_index("choice")];
903 var cpno = parseInt(choice.getAttribute("choicepointno"));
904 var choiceno = parseInt(choice.getAttribute("choiceno"));
905 var choicedesc = choice.getAttribute("desc");
907 var title = "<H3>Error diagnostics</H3>";
909 if (is_defined(choicedesc) && choicedesc != null) {
910 subtitle = "<p>Errors at node " + cpno + " = " + choicedesc + "</p>";
912 subtitle = "<p>Global errors:</p>";
915 disambcell.innerHTML = title + subtitle;
916 var failures = get_failure_opts(cpno,choiceno);
917 for (var i = 0;i < failures.length;i++) {
918 disambcell.appendChild(failures[i]);
919 disambcell.appendChild(document.createTextNode(failures[i].getAttribute("title")));
920 disambcell.appendChild(document.createElement("br"));
923 var okbutton = document.createElement("input");
924 okbutton.setAttribute("type","button");
925 okbutton.setAttribute("value","Show error loc");
926 okbutton.setAttribute("onclick","show_err()");
927 var cancelbutton = document.createElement("input");
928 cancelbutton.setAttribute("type","button");
929 cancelbutton.setAttribute("value","Close");
930 cancelbutton.setAttribute("onclick","cancel_disambiguate()");
931 var backbutton = document.createElement("input");
932 backbutton.setAttribute("type","button");
933 backbutton.setAttribute("value","<< Back");
934 backbutton.setAttribute("onclick","next_cp(" + cpno + ")");
936 disambcell.appendChild(backbutton);
937 disambcell.appendChild(okbutton);
938 disambcell.appendChild(cancelbutton);
942 function show_err() {
943 var radios = document.getElementsByName("failure");
944 for (i = 0; i < radios.length; i++) {
945 if (radios[i].checked) {
946 var start = radios[i].getAttribute("start");
947 var stop = radios[i].getAttribute("stop");
948 var title = radios[i].getAttribute("title");
949 var unlockedtxt = matita.unlockedbackup;
950 var pre = unlockedtxt.substring(0,start).matita_to_html();
951 var mid = unlockedtxt.substring(start,stop).matita_to_html();
952 var post = unlockedtxt.substring(stop).matita_to_html();
953 unlocked.innerHTML = pre +
954 "<span class=\"error\" title=\"Disambiguation failure\">" +
955 mid + "</span>" + post;
961 function gotoBottom()
963 processor = function(xml) {
964 if (is_defined(xml)) {
965 // debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND");
966 var parsed = xml.getElementsByTagName("parsed");
967 var localized = xml.getElementsByTagName("localized")[0];
968 var ambiguity = xml.getElementsByTagName("ambiguity")[0];
969 var generic_err = xml.getElementsByTagName("error")[0];
970 var disamberr = xml.getElementsByTagName("disamberror")[0];
971 for (var i = 0;i < parsed.length; i++) {
972 var len = parsed[i].getAttribute("length");
973 // len0 = unlocked.innerHTML.length;
974 var unescaped = unlocked.innerHTML.html_to_matita();
975 // the browser may decide to split textnodes: use wholeText!
976 var parsedtxt = parsed[i].childNodes[0].wholeText;
977 //parsedtxt = unescaped.substr(0,len);
978 var unparsedtxt = unescaped.substr(len);
979 lockedbackup += parsedtxt;
980 locked.innerHTML = lockedbackup; //.matita_to_html();
981 unlocked.innerHTML = unparsedtxt.matita_to_html();
982 // len1 = unlocked.innerHTML.length;
983 var len2 = parsedtxt.length;
984 statements = listcons(len2,statements);
986 // unlocked.scrollIntoView(true);
988 metasenv = xml.getElementsByTagName("meta");
991 populate_goalarray(metasenv);
993 if (is_defined(ambiguity)) {
994 var start = parseInt(ambiguity.getAttribute("start"));
995 var stop = parseInt(ambiguity.getAttribute("stop"));
996 var choices = xml.getElementsByTagName("choice");
998 matita.ambiguityStart = start;
999 matita.ambiguityStop = stop;
1000 matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
1001 matita.interpretations = [];
1003 var unlockedtxt = unlocked.innerHTML.html_to_matita();
1004 var pre = unlockedtxt.substring(0,start).matita_to_html();
1005 var mid = unlockedtxt.substring(start,stop).matita_to_html();
1006 var post = unlockedtxt.substring(stop).matita_to_html();
1007 unlocked.innerHTML = pre +
1008 "<span class=\"error\" title=\"disambiguation error\">" +
1009 mid + "</span>" + post;
1011 var title = "<H3>Ambiguous input</H3>";
1012 disambcell.innerHTML = title;
1013 for (i = 0;i < choices.length;i++) {
1014 matita.interpretations[i] = new Object();
1016 var href = choices[i].getAttribute("href");
1017 var title = choices[i].getAttribute("title");
1018 var desc = choices[i].childNodes[0].nodeValue;
1020 matita.interpretations[i].href = href;
1021 matita.interpretations[i].title = title;
1022 matita.interpretations[i].desc = desc;
1024 var choice = document.createElement("input");
1025 choice.setAttribute("type","radio");
1026 choice.setAttribute("name","interpr");
1027 choice.setAttribute("href",href);
1028 choice.setAttribute("title",title);
1029 if (i == 0) choice.setAttribute("checked","");
1031 disambcell.appendChild(choice);
1032 disambcell.appendChild(document.createTextNode(desc));
1033 disambcell.appendChild(document.createElement("br"));
1036 var okbutton = document.createElement("input");
1037 okbutton.setAttribute("type","button");
1038 okbutton.setAttribute("value","OK");
1039 okbutton.setAttribute("onclick","do_disambiguate()");
1040 var cancelbutton = document.createElement("input");
1041 cancelbutton.setAttribute("type","button");
1042 cancelbutton.setAttribute("value","Cancel");
1043 cancelbutton.setAttribute("onclick","cancel_disambiguate()");
1045 disambcell.appendChild(okbutton);
1046 disambcell.appendChild(cancelbutton);
1048 matita.disambMode = true;
1051 else if (is_defined(disamberr)) {
1052 // must be fixed in a daemon: it makes sense to return a
1053 // disambiguation error with no choices
1054 if (disamberr.childNodes.length > 0) {
1055 set_cps(disamberr.childNodes);
1056 matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
1057 matita.disambMode = true;
1062 else if (is_defined(localized)) {
1063 unlocked.innerHTML = localized.childNodes[0].wholeText;
1065 else if (is_defined(generic_err)) {
1066 error("Unmanaged error:\n" + generic_err.childNodes[0].wholeText);
1069 error("goto bottom failed");
1074 callServer("bottom",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
1080 processor = function(xml) {
1081 if (is_defined(xml)) {
1082 if (xml.childNodes[0].textContent != "ok") {
1083 error("goto top failed");
1086 statements = listnil();
1088 lockedlen = locked.innerHTML.length - statementlen;
1089 statement = locked.innerHTML.substr(lockedlen, statementlen);
1090 locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
1091 unlocked.innerHTML = statement + unlocked.innerHTML;
1093 unlocked.innerHTML = lockedbackup + unlocked.innerHTML;
1095 locked.innerHTML = lockedbackup;
1100 // unlocked.scrollIntoView(true);
1103 error("goto top failed");
1108 callServer("top",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
1112 function gotoPos(offset)
1114 if (!is_defined(offset)) {
1115 offset = getCursorPos();
1117 processor = function(xml) {
1118 if (is_defined(xml)) {
1120 var len = advOneStep(xml);
1121 if (offset <= len) {
1124 populate_goalarray(metasenv);
1127 gotoPos(offset - len);
1132 populate_goalarray(metasenv);
1138 // unlocked.scrollIntoView(true);
1140 populate_goalarray(metasenv);
1145 callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
1148 function retractStep()
1150 processor = function(xml) {
1151 if (typeof xml != "undefined") {
1152 // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
1153 statementlen = parseInt(listhd(statements));
1154 statements = listtl(statements);
1156 lockedlen = locked.innerHTML.length - statementlen;
1157 statement = locked.innerHTML.substr(lockedlen, statementlen);
1158 locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
1159 unlocked.innerHTML = statement + unlocked.innerHTML;
1161 lockedlen = lockedbackup.length - statementlen;
1162 statement = lockedbackup.substr(lockedlen, statementlen);
1163 lockedbackup = lockedbackup.substr(0,lockedlen);
1164 locked.innerHTML = lockedbackup;
1165 unlocked.innerHTML = statement + unlocked.innerHTML;
1166 metasenv = xml.getElementsByTagName("meta");
1167 populate_goalarray(metasenv);
1171 // unlocked.scrollIntoView(true);
1174 error("retract failed");
1179 callServer("retract",processor);
1184 processor = function(xml)
1186 if (is_defined(xml)) {
1188 locked.innerHTML = lockedbackup;
1189 unlocked.innerHTML = xml.documentElement.wholeText;
1192 error("file open failed");
1195 callServer("open",processor,"file=" + escape(filename.value));
1198 function retrieveFile(thefile)
1200 processor = function(xml)
1202 if (is_defined(xml)) {
1203 if (!is_defined(xml.getElementsByTagName("error")[0])) {
1204 changeFile(thefile);
1205 matita.disambMode = false;
1206 matita.proofMode = false;
1209 locked.innerHTML = lockedbackup;
1210 // code originally used in google chrome (problems with mozilla)
1211 // debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
1212 // unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
1213 debug(xml.childNodes[0].textContent);
1214 if (document.all) { // IE
1215 unlocked.innerHTML = xml.childNodes[0].text;
1217 unlocked.innerHTML = xml.childNodes[0].textContent;
1224 error("file open failed");
1227 window.location = "/login.html";
1230 abortDialog("dialogBox");
1231 callServer("open",processor,"file=" + escape(thefile));
1234 function go_external_hyperlink(uri,thefile,id)
1236 processor = function(xml)
1238 if (is_defined(xml)) {
1239 // code originally used in google chrome (problems with mozilla)
1240 // debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
1241 // unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
1242 // debug(xml.childNodes[0].textContent);
1244 if (document.all) { // IE
1245 doctext = xml.childNodes[0].text;
1247 doctext= xml.childNodes[0].textContent;
1249 $('#locked').html(doctext);
1251 // scroll to anchor (if it exists)
1252 $('#' + id).scrollIntoView(true);
1257 $('#locked').html("404 object not found");
1260 callServer("open",processor,"file=" + escape(thefile) + "&readonly=true");
1263 function createDocWin(uri,id) {
1264 // 12 = position of the second '/' in uri (to strip off "cic:/matita/")
1265 var thefile = uri.substring(12) + ".ma";
1266 var title = "Matita Browser - " + uri;
1267 var docWin = window.open( "", "matitabrowser",
1268 "width=800,height=600,location=no,menubar=no,status=no,scrollbars,resizable,screenX=20,screenY=40,left=20,top=40");
1269 docWin.document.write('<html><head><title>' + title + '</title>' +
1270 '<script type="text/javascript" src="jquery.js"></script>' +
1271 '<script type="text/javascript" src="jquery.tooltip.min.js"></script>' +
1272 '<script type="text/javascript" src="matitaweb.js"></script>' +
1273 '<script type="text/javascript">go_external_hyperlink("' + uri + '","' + thefile + '","' + id + '");</script>' +
1274 '<link rel="stylesheet" type="text/css" href="matitaweb.css"/>' +
1275 '<link rel="stylesheet" type="text/css" href="jquery.tooltip.css"/>' +
1277 docWin.document.write('<body><H1>'+ uri + '</H1>' +
1278 '<pre id="locked"></pre></body></html>');
1279 docWin.document.close();
1280 docWin.baseuri = uri;
1284 function showLibrary(title,callback,reloadDialog)
1287 dialogBox.reload = reloadDialog;
1289 if (window.XMLHttpRequest)
1291 req = new XMLHttpRequest();
1293 else if (window.ActiveXObject)
1296 req = new ActiveXObject("Msxml2.XMLHTTP");
1300 req = new ActiveXObject("Microsoft.XMLHTTP");
1304 req.onreadystatechange = function()
1307 rs = req.readyState;
1312 stxt = req.statusText;
1315 debug(req.responseText);
1316 showDialog("<H2>" + title + "</H2>",req.responseText, callback);
1320 req.open("POST", "viewlib"); // + escape(unlocked.innerHTML), true);
1321 req.setRequestHeader("Content-type","application/x-www-form-urlencoded");
1326 function uploadDialog()
1328 uploadBox.style.display = "block";
1333 var file = document.getElementById("uploadFilename").files[0];
1335 // var filecontent = file.getAsText("UTF-8");
1336 // locked.innerHTML = lockedbackup;
1337 // unlocked.innerHTML = filecontent;
1338 // uploadBox.style.display = "none";
1341 var reader = new FileReader();
1342 reader.onerror = function (evt) {
1343 error("file open failed");
1345 reader.onload = function (evt) {
1347 locked.innerHTML = lockedbackup
1348 unlocked.innerHTML = "";
1349 unlocked.appendChild(document.createTextNode(evt.target.result));
1350 uploadBox.style.display = "none";
1352 try { reader.readAsText(file, "UTF-8"); }
1353 catch (err) { /* nothing to do */ };
1354 uploadBox.style.display = "none";
1358 function openDialog()
1360 callback = function (fname) { retrieveFile(fname); };
1361 showLibrary("Open file", callback, openDialog);
1364 function saveDialog()
1366 callback = function (fname) {
1367 abortDialog("dialogBox");
1369 (locked.innerHTML.html_to_matita()).sescape(),
1370 (unlocked.innerHTML.html_to_matita()).sescape(),
1373 showLibrary("Save file as", callback, saveDialog);
1376 function newDialog()
1378 callback = function (fname) {
1379 abortDialog("dialogBox");
1380 saveFile(fname,"","",false,newDialog,true);
1382 showLibrary("Create new file", callback, newDialog);
1386 function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog,reloadFile)
1388 if (!is_defined(reloadFile)) { reloadFile = true };
1389 if (!is_defined(fname)) {
1390 fname = current_fname;
1391 lockedtxt = (locked.innerHTML.html_to_matita()).sescape();
1392 unlockedtxt = (unlocked.innerHTML.html_to_matita()).sescape();
1394 // when force is true, reloadDialog is not needed
1396 processor = function(xml) {
1397 if (is_defined(xml)) {
1398 if (xml.childNodes[0].textContent != "ok") {
1399 if (confirm("File already exists. All existing data will be lost.\nDo you want to proceed anyway?")) {
1400 saveFile(fname,lockedtxt,unlockedtxt,true,reloadDialog,reloadFile);
1406 debug("file saved!");
1407 if (reloadFile) { retrieveFile(fname); }
1410 error("save file failed");
1414 if (is_defined(fname)) {
1416 callServer("save",processor,"file=" + escape(fname) +
1417 "&locked=" + lockedtxt +
1418 "&unlocked=" + unlockedtxt +
1421 else { error("no file selected"); }
1424 function createDir() {
1425 abortDialog("dialogBox");
1426 dirname = prompt("New directory name:\ncic:/matita/","newdir");
1427 if (dirname != null) {
1428 processor = function(xml) {
1429 if (is_defined(xml)) {
1430 if (xml.childNodes[0].textContent != "ok") {
1431 alert("An error occurred :-(");
1434 alert("An error occurred :-(");
1439 callServer("save",processor,"file=" + escape(dirname) +
1440 "&locked=&unlocked=&force=false&dir=true");
1446 function commitAll()
1448 processor = function(xml) {
1449 if (is_defined(xml)) {
1450 debug(xml.getElementsByTagName("details")[0].textContent);
1451 alert("Commit executed: see details in the log.\n\n" +
1452 "NOTICE: this message does NOT imply (yet) that the commit was successful.");
1454 alert("Commit failed!");
1459 callServer("commit",processor);
1462 function updateAll()
1464 processor = function(xml) {
1465 if (is_defined(xml)) {
1466 alert("Update executed.\n\n" +
1468 xml.getElementsByTagName("details")[0].textContent);
1470 alert("Update failed!");
1475 callServer("update",processor);
1480 function hideSequent() {
1481 matita.proofMode = false;
1485 function showSequent() {
1486 matita.proofMode = true;
1490 function showDialog(title,content,callback) {
1491 dialogTitle.innerHTML = title;
1492 dialogContent.innerHTML = content;
1493 dialogBox.callback = callback;
1495 //Get the screen height and width
1496 var maskHeight = $(document).height();
1497 var maskWidth = $(window).width();
1499 //Set heigth and width to mask to fill up the whole screen
1500 $('#mask').css({'width':maskWidth,'height':maskHeight});
1503 $('#mask').fadeIn(100);
1504 $('#mask').fadeTo(200,0.8);
1506 //Get the window height and width
1507 var winH = $(window).height();
1508 var winW = $(window).width();
1510 //Set the popup window to center
1511 $('#dialogBox').css('top', winH/2-$('#dialogBox').height()/2);
1512 $('#dialogBox').css('left', winW/2-$('#dialogBox').width()/2);
1515 $('#dialogBox').fadeIn(200);
1517 dialogBox.style.display = "block";
1520 function abortDialog(dialog) {
1521 document.getElementById(dialog).style.display = "none";
1525 function removeElement(id) {
1526 var element = document.getElementById(id);
1527 element.parentNode.removeChild(element);
1533 function getCursorPos() {
1535 if (window.getSelection) {
1536 var selObj = window.getSelection();
1537 savedRange = selObj.getRangeAt(0);
1538 savedsc = savedRange.startContainer;
1539 savedso = savedRange.startOffset;
1540 //cursorPos = findNode(selObj.anchorNode.parentNode.childNodes, selObj.anchorNode) + selObj.anchorOffset;
1541 cursorPos = findNode(unlocked.childNodes, selObj.anchorNode,0) + selObj.anchorOffset;
1542 /* FIXME the following works wrong in Opera when the document is longer than 32767 chars */
1545 else if (document.selection) {
1546 savedRange = document.selection.createRange();
1547 var bookmark = savedRange.getBookmark();
1548 /* FIXME the following works wrong when the document is longer than 65535 chars */
1549 cursorPos = bookmark.charCodeAt(2) - 11; /* Undocumented function [3] */
1554 function findNode(list, node, acc) {
1555 for (var i = 0; i < list.length; i++) {
1556 if (list[i] == node) {
1557 // debug("success " + i);
1560 if (list[i].hasChildNodes()) {
1562 // debug("recursion on node " + i);
1563 return (findNode(list[i].childNodes,node,acc))
1565 catch (e) { /* debug("recursion failed"); */ }
1567 sandbox = document.getElementById("sandbox");
1568 dup = list[i].cloneNode(true);
1569 sandbox.appendChild(dup);
1570 // debug("fail " + i + ": " + sandbox.innerHTML);
1571 acc += sandbox.innerHTML.html_to_matita().length;
1572 sandbox.removeChild(dup);
1578 debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos()));
1581 function get_checked_index(name) {
1582 var radios = document.getElementsByName(name);
1583 for (i = 0; i < radios.length; i++) {
1584 if (radios[i].checked) {
1591 function cancel_disambiguate() {
1592 matita.disambMode = false;
1594 // enable_toparea();
1595 // enable_editing();
1596 strip_tags("span","error");
1600 function do_disambiguate() {
1601 var i = get_checked_index("interpr");
1603 var pre = matita.unlockedbackup
1604 .substring(0,matita.ambiguityStart).matita_to_html();
1605 var mid = matita.unlockedbackup
1606 .substring(matita.ambiguityStart,matita.ambiguityStop)
1608 var post = matita.unlockedbackup
1609 .substring(matita.ambiguityStop).matita_to_html();
1611 var href = matita.interpretations[i].href;
1612 var title = matita.interpretations[i].title;
1614 if (is_defined(title)) {
1615 mid = "<A href=\"" + href + "\" title=\"" + title + "\">" + mid + "</A>";
1617 mid = "<A href=\"" + href + "\">" + mid + "</A>";
1620 unlocked.innerHTML = pre + mid + post;
1622 matita.disambMode = false;
1629 function do_showerror() {
1630 var i = get_checked_index("choice");
1632 var pre = matita.unlockedbackup
1633 .substring(0,matita.ambiguityStart).matita_to_html();
1634 var mid = matita.unlockedbackup
1635 .substring(matita.ambiguityStart,matita.ambiguityStop)
1637 var post = matita.unlockedbackup
1638 .substring(matita.ambiguityStop).matita_to_html();
1640 var href = matita.interpretations[i].href;
1641 var title = matita.interpretations[i].title;
1643 if (is_defined(title)) {
1644 mid = "<A href=\"" + href + "\" title=\"" + title + "\">" + mid + "</A>";
1646 mid = "<A href=\"" + href + "\">" + mid + "</A>";
1649 unlocked.innerHTML = pre + mid + post;
1654 function readCookie(name) {
1655 var nameEQ = name + "=";
1656 var ca = document.cookie.split(';');
1657 for(var i=0;i < ca.length;i++) {
1659 while (c.charAt(0)==' ') c = c.substring(1,c.length);
1660 if (c.indexOf(nameEQ) == 0) return c.substring(nameEQ.length,c.length);
1665 function delete_cookie ( cookie_name )
1667 var cookie_date = new Date(); // current date & time
1668 cookie_date.setTime ( cookie_date.getTime() - 1 );
1669 document.cookie = cookie_name += "=; expires=" + cookie_date.toGMTString();
1672 function delete_session()
1674 delete_cookie("session");
1677 function disable_toparea() {
1678 var offset = $('#toparea').offset();
1679 $('#whitemask').css('top',offset.top);
1680 $('#whitemask').css('left',offset.left);
1681 $('#whitemask').css('width',$('#toparea').outerWidth() + "px");
1682 $('#whitemask').css('height',$('#toparea').outerHeight() + "px");
1683 $('#whitemask').fadeTo('fast',0.7);
1686 function enable_toparea() {
1687 $('#whitemask').hide();
1690 function disable_editing() {
1691 unlocked.contentEditable = false;
1694 function enable_editing() {
1695 unlocked.contentEditable = true;
1700 // advanceButton.disabled = true;
1701 // retractButton.disabled = true;
1702 // cursorButton.disabled = true;
1703 // bottomButton.disabled = true;
1710 // advanceButton.disabled = false;
1711 // retractButton.disabled = false;
1712 // cursorButton.disabled = false;
1713 // bottomButton.disabled = false;
1714 if (!matita.disambMode) {