21 if (readCookie("session") == null) {
22 window.location = "/login.html"
24 locked = document.getElementById("locked");
25 unlocked = document.getElementById("unlocked");
26 workarea = document.getElementById("workarea");
27 scriptcell = document.getElementById("scriptcell");
28 goalcell = document.getElementById("goalcell");
29 goals = document.getElementById("goals");
30 goalview = document.getElementById("goalview");
31 filename = document.getElementById("filename");
32 logarea = document.getElementById("logarea");
33 advanceButton = document.getElementById("advance");
34 retractButton = document.getElementById("retract");
35 cursorButton = document.getElementById("cursor");
36 bottomButton = document.getElementById("bottom");
37 dialogBox = document.getElementById("dialogBox");
38 dialogTitle = document.getElementById("dialogTitle");
39 dialogContent = document.getElementById("dialogContent");
41 // hide sequent view at start
44 // initialize keyboard events in the unlocked script
45 init_keyboard(unlocked);
49 function init_keyboard(target)
51 if (target.addEventListener)
53 // target.addEventListener("keydown",keydown,false);
54 target.addEventListener("keypress",keypress,false);
55 // target.addEventListener("keyup",keyup,false);
56 // target.addEventListener("textInput",textinput,false);
58 else if (target.attachEvent)
60 // target.attachEvent("onkeydown", keydown);
61 target.attachEvent("onkeypress", keypress);
62 // target.attachEvent("onkeyup", keyup);
63 // target.attachEvent("ontextInput", textinput);
67 // target.onkeydown= keydown;
68 target.onkeypress= keypress;
69 // target.onkeyup= keyup;
70 // target.ontextinput= textinput; // probably doesn't work
77 if (n == null) return 'undefined';
79 if (n >= 32 && n < 127) s+= ' (' + String.fromCharCode(n) + ')';
80 while (s.length < 9) s+= ' ';
84 function string_of_key(n)
86 if (n == null) return 'undefined';
87 return String.fromCharCode(n);
90 function pressmesg(w,e)
92 debug(w + ' keyCode=' + keyval(e.keyCode) +
93 ' which=' + keyval(e.which) +
94 ' charCode=' + keyval(e.charCode) +
95 '\n shiftKey='+e.shiftKey
96 + ' ctrlKey='+e.ctrlKey
98 + ' metaKey='+e.metaKey);
101 function suppressdefault(e,flag)
105 if (e.preventDefault) e.preventDefault();
106 if (e.stopPropagation) e.stopPropagation();
114 pressmesg('keypress',e);
115 var s = string_of_key(e.charCode);
117 i = unlocked.innerHTML.lastIndexOf('\\',getCursorPos());
119 window.alert("found " + unlocked.innerHTML.substring(i,getCursorPos()));
121 return suppressdefault(e,true);
123 return suppressdefault(e,false);
129 // internet explorer (v.9) doesn't work with innerHTML
130 // but google chrome's innerText is, in a sense, "write only"
131 // what should we do?
132 logarea.innerText = txt + "\n" + logarea.innerText;
138 debug("hd of '" + l + "' = '" + ar[0] + "'");
146 debug("tl of '" + l + "' = '" + tl + "'");
150 function listcons(x,l)
152 debug("cons '" + x + "' on '" + l + "'");
153 return (x + "#" + l);
166 function fold_left (f,acc,l)
169 { debug("'" + l + "' is fold end");
172 { debug("'" + l + "' is fold cons");
173 return(fold_left (f,f(acc,(listhd(l))),listtl(l))); }
176 function listiter (f,l)
179 { debug("'" + l + "' is nil");
184 debug("'" + l + "' is not nil");
186 listiter(f,listtl(l));
190 function listmap (f,l)
192 debug("listmap on " + l);
194 { debug("returning listnil");
198 { debug("cons f(hd) map(f,tl)");
199 return(f(listhd(l)) + "#" + listmap(f,listtl(l)));
203 var statements = listnil();
206 var metalist = listnil();
208 function pairmap (f,p)
210 debug("pairmap of '" + p + "'");
212 return (f(ar[0],ar[1]));
215 function tripletmap (f,p)
217 debug("tripletmap of '" + p + "'");
219 return (f(ar[0],ar[1],ar[2]));
225 return (pairmap (function (a,b) { return (a); }, p));
231 return (tripletmap (function (a,b,c) { return (a); }, p));
237 return (tripletmap (function (a,b,c) { return (b); }, p));
243 return (tripletmap (function (a,b,c) { return (c); }, p));
246 function populate_goalarray(menv)
248 debug("metasenv.length = " + menv.length);
249 if (menv.length == 0) {
255 goalarray = new Array();
256 metalist = listnil();
257 var tmp_goallist = "";
258 for (i = 0; i < menv.length; i++) {
259 metano = menv[i].getAttribute("number");
260 metaname = menv[i].childNodes[0].childNodes[0].data;
261 goal = menv[i].childNodes[1].childNodes[0].data;
262 debug ("found meta n. " + metano);
263 debug ("found goal\nBEGIN" + goal + "\nEND");
264 goalarray[metano] = goal;
265 tmp_goallist = " <A href=\"javascript:switch_goal(" + metano + ")\">" + metaname + "</A>" + tmp_goallist;
266 metalist = listcons(metano,metalist);
267 debug ("goalarray[\"" + metano + "\"] = " + goalarray[metano]);
269 goals.innerHTML = tmp_goallist;
270 debug("new metalist is '" + metalist + "'");
271 if (is_nil(metalist)) {
275 switch_goal(listhd(metalist));
280 function switch_goal(meta)
282 if (typeof meta == "undefined") {
283 goalview.innerHTML = "";
286 debug("switch_goal " + meta + "\n" + goalarray[meta]);
287 goalview.innerHTML = "<B>Goal ?" + meta + ":</B>\n\n" + goalarray[meta];
291 String.prototype.sescape = function() {
297 result = result.replace(patt1,"%25");
298 result = result.replace(patt2,"%3D");
299 result = result.replace(patt3,"%26");
300 result = result.replace(patt4,"%2B");
304 String.prototype.unescapeHTML = function()
306 var patt1 = /<br(\/|)>/gi;
307 var patt2 = /</gi;
308 var patt3 = />/gi;
310 result = result.replace(patt1,"\n");
311 result = result.replace(patt2,"<");
312 result = result.replace(patt3,">");
313 return (unescape(result));
318 advanceButton.disabled = true;
319 retractButton.disabled = true;
320 cursorButton.disabled = true;
321 bottomButton.disabled = true;
326 advanceButton.disabled = false;
327 retractButton.disabled = false;
328 cursorButton.disabled = false;
329 bottomButton.disabled = false;
332 function is_defined(x)
334 return (typeof x != "undefined");
337 /* servicename: name of the service being called
338 * reqbody: text of the request
339 * processResponse: processes the server response
340 * (takes the response text in input, undefined in case of error)
342 function callServer(servicename,processResponse,reqbody)
346 if (window.XMLHttpRequest)
348 req = new XMLHttpRequest();
350 else if (window.ActiveXObject)
353 req = new ActiveXObject("Msxml2.XMLHTTP");
357 req = new ActiveXObject("Microsoft.XMLHTTP");
361 req.onreadystatechange = function()
369 stxt = req.statusText;
372 debug(req.responseText);
373 if (window.DOMParser) {
374 parser=new DOMParser();
375 xmlDoc=parser.parseFromString(req.responseText,"text/xml");
377 else // Internet Explorer
379 xmlDoc=new ActiveXObject("Microsoft.XMLDOM");
380 xmlDoc.async="false";
381 xmlDoc.loadXML(req.responseText);
383 processResponse(xmlDoc);
389 req.open("POST", servicename); // + escape(unlocked.innerHTML), true);
390 req.setRequestHeader("Content-type","application/x-www-form-urlencoded");
399 function advanceForm1()
401 processor = function(xml) {
402 if (is_defined(xml)) {
403 // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
404 len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length"));
405 len0 = unlocked.innerHTML.length;
406 unescaped = unlocked.innerHTML.unescapeHTML();
407 parsedtxt = unescaped.substr(0,len);
408 unparsedtxt = unescaped.substr(len);
409 locked.innerHTML = locked.innerHTML + parsedtxt;
410 unlocked.innerHTML = unparsedtxt;
411 len1 = unlocked.innerHTML.length;
413 metasenv = xml.getElementsByTagName("meta");
414 populate_goalarray(metasenv);
415 statements = listcons(len2,statements);
416 unlocked.scrollIntoView(true);
418 debug("advance failed");
423 callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape());
427 function gotoBottom()
429 processor = function(xml) {
430 if (is_defined(xml)) {
431 // debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND");
432 len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length"));
433 len0 = unlocked.innerHTML.length;
434 unescaped = unlocked.innerHTML.unescapeHTML();
435 parsedtxt = unescaped.substr(0,len);
436 unparsedtxt = unescaped.substr(len);
437 locked.innerHTML = locked.innerHTML + parsedtxt;
438 unlocked.innerHTML = unparsedtxt;
439 len1 = unlocked.innerHTML.length;
441 metasenv = xml.getElementsByTagName("meta");
442 populate_goalarray(metasenv);
443 statements = listcons(len2,statements);
444 unlocked.scrollIntoView(true);
446 debug("goto bottom failed");
451 callServer("bottom",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape());
456 function gotoPos(offset)
458 if (!is_defined(offset)) {
459 offset = getCursorPos();
461 processor = function(xml) {
462 if (is_defined(xml)) {
463 // debug("goto pos: received response\nBEGIN\n" + req.responseText + "\nEND");
464 len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length"));
465 len0 = unlocked.innerHTML.length;
466 unescaped = unlocked.innerHTML.unescapeHTML();
467 parsedtxt = unescaped.substr(0,len);
468 unparsedtxt = unescaped.substr(len);
469 locked.innerHTML = locked.innerHTML + parsedtxt;
470 unlocked.innerHTML = unparsedtxt;
471 len1 = unlocked.innerHTML.length;
473 metasenv = xml.getElementsByTagName("meta");
474 // populate_goalarray(metasenv);
475 statements = listcons(len2,statements);
476 unlocked.scrollIntoView(true);
477 // la populate non andrebbe fatta a ogni passo
479 populate_goalarray(metasenv);
482 gotoPos(offset - len);
485 unlocked.scrollIntoView(true);
486 populate_goalarray(metasenv);
491 callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape());
496 processor = function(xml) {
497 if (typeof xml != "undefined") {
498 // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
499 statementlen = parseInt(listhd(statements));
500 statements = listtl(statements);
501 lockedlen = locked.innerHTML.length - statementlen;
502 statement = locked.innerHTML.substr(lockedlen, statementlen);
503 locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
504 unlocked.innerHTML = statement + unlocked.innerHTML;
505 metasenv = xml.getElementsByTagName("meta");
506 populate_goalarray(metasenv);
507 unlocked.scrollIntoView(true);
509 debug("retract failed");
515 callServer("retract",processor);
521 processor = function(xml)
523 if (is_defined(xml)) {
524 locked.innerHTML = "";
525 unlocked.innerHTML = xml.documentElement.textContent;
527 debug("file open failed");
530 callServer("open",processor,"file=" + escape(filename.value));
533 function retrieveFile(thefile)
535 processor = function(xml)
537 if (is_defined(xml)) {
538 locked.innerHTML = "";
539 unlocked.innerHTML = xml.documentElement.textContent;
541 debug("file open failed");
544 dialogBox.style.display = "none";
545 callServer("open",processor,"file=" + escape(thefile));
548 function showLibrary()
552 if (window.XMLHttpRequest)
554 req = new XMLHttpRequest();
556 else if (window.ActiveXObject)
559 req = new ActiveXObject("Msxml2.XMLHTTP");
563 req = new ActiveXObject("Microsoft.XMLHTTP");
567 req.onreadystatechange = function()
575 stxt = req.statusText;
578 debug(req.responseText);
579 showDialog("<H2>Library</H2>",req.responseText);
583 req.open("POST", "viewlib"); // + escape(unlocked.innerHTML), true);
584 req.setRequestHeader("Content-type","application/x-www-form-urlencoded");
591 function hideSequent() {
592 goalcell.parentNode.removeChild(goalcell);
593 scriptcell.setAttribute("colspan","2");
596 function showSequent() {
597 scriptcell.setAttribute("colspan","1");
598 workarea.appendChild(goalcell);
601 function showDialog(title,content) {
602 dialogTitle.innerHTML = title;
603 dialogContent.innerHTML = content;
604 dialogBox.style.display = "block";
607 function removeElement(id) {
608 var element = document.getElementById(id);
609 element.parentNode.removeChild(element);
612 function getCursorPos() {
614 if (window.getSelection) {
615 var selObj = window.getSelection();
616 var selRange = selObj.getRangeAt(0);
617 //cursorPos = findNode(selObj.anchorNode.parentNode.childNodes, selObj.anchorNode) + selObj.anchorOffset;
618 cursorPos = findNode(unlocked.childNodes, selObj.anchorNode,0) + selObj.anchorOffset;
619 /* FIXME the following works wrong in Opera when the document is longer than 32767 chars */
622 else if (document.selection) {
623 var range = document.selection.createRange();
624 var bookmark = range.getBookmark();
625 /* FIXME the following works wrong when the document is longer than 65535 chars */
626 cursorPos = bookmark.charCodeAt(2) - 11; /* Undocumented function [3] */
631 function findNode(list, node, acc) {
632 for (var i = 0; i < list.length; i++) {
633 if (list[i] == node) {
634 // debug("success " + i);
637 if (list[i].hasChildNodes()) {
639 // debug("recursion on node " + i);
640 return (findNode(list[i].childNodes,node,acc))
642 catch (e) { /* debug("recursion failed"); */ }
644 sandbox = document.getElementById("sandbox");
645 dup = list[i].cloneNode(true);
646 sandbox.appendChild(dup);
647 // debug("fail " + i + ": " + sandbox.innerHTML);
648 acc += sandbox.innerHTML.length;
649 sandbox.removeChild(dup);
655 debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos()));
658 function readCookie(name) {
659 var nameEQ = name + "=";
660 var ca = document.cookie.split(';');
661 for(var i=0;i < ca.length;i++) {
663 while (c.charAt(0)==' ') c = c.substring(1,c.length);
664 if (c.indexOf(nameEQ) == 0) return c.substring(nameEQ.length,c.length);
669 function delete_cookie ( cookie_name )
671 var cookie_date = new Date(); // current date & time
672 cookie_date.setTime ( cookie_date.getTime() - 1 );
673 document.cookie = cookie_name += "=; expires=" + cookie_date.toGMTString();
676 function delete_session()
678 delete_cookie("session");