6 <script language="JavaScript">
23 locked = document.getElementById("locked");
24 unlocked = document.getElementById("unlocked");
25 workarea = document.getElementById("workarea");
26 scriptcell = document.getElementById("scriptcell");
27 goalcell = document.getElementById("goalcell");
28 goals = document.getElementById("goals");
29 goalview = document.getElementById("goalview");
30 filename = document.getElementById("filename");
31 logarea = document.getElementById("logarea");
32 advanceButton = document.getElementById("advance");
33 retractButton = document.getElementById("retract");
34 cursorButton = document.getElementById("cursor");
35 bottomButton = document.getElementById("bottom");
37 // hide sequent view at start
43 logarea.innerHTML = txt + "\n" + logarea.innerHTML;
49 debug("hd of '" + l + "' = '" + ar[0] + "'");
57 debug("tl of '" + l + "' = '" + tl + "'");
61 function listcons(x,l)
63 debug("cons '" + x + "' on '" + l + "'");
77 function fold_left (f,acc,l)
80 { debug("'" + l + "' is fold end");
83 { debug("'" + l + "' is fold cons");
84 return(fold_left (f,f(acc,(listhd(l))),listtl(l))); }
87 function listiter (f,l)
90 { debug("'" + l + "' is nil");
95 debug("'" + l + "' is not nil");
97 listiter(f,listtl(l));
101 function listmap (f,l)
103 debug("listmap on " + l);
105 { debug("returning listnil");
109 { debug("cons f(hd) map(f,tl)");
110 return(f(listhd(l)) + "#" + listmap(f,listtl(l)));
114 var statements = listnil();
117 var metalist = listnil();
119 function pairmap (f,p)
121 debug("pairmap of '" + p + "'");
123 return (f(ar[0],ar[1]));
126 function tripletmap (f,p)
128 debug("tripletmap of '" + p + "'");
130 return (f(ar[0],ar[1],ar[2]));
136 return (pairmap (function (a,b) { return (a); }, p));
142 return (tripletmap (function (a,b,c) { return (a); }, p));
148 return (tripletmap (function (a,b,c) { return (b); }, p));
154 return (tripletmap (function (a,b,c) { return (c); }, p));
157 function populate_goalarray(txt)
165 debug("populate with '" + txt + "'");
166 goalarray = new Array();
167 metalist = listnil();
168 var tmp_goallist = "";
169 listiter (function(item)
171 debug ("item is '" + item + "'");
172 tripletmap (function(a,ahtml,b) {
173 debug ("found meta n. " + a);
174 debug ("found goal\nBEGIN" + unescape(b) + "\nEND");
175 goalarray[a] = unescape(b);
176 tmp_goallist = " <A href=\"javascript:switch_goal(" + a + ")\">" + unescape(ahtml) + "</A>" + tmp_goallist;
177 metalist = listcons(a,metalist);
178 debug ("goalarray[\"" + a + "\"] = " + goalarray[a]);
181 // metalist = listmap (p13,txt);
182 goals.innerHTML = tmp_goallist;
183 debug("new metalist is '" + metalist + "'");
184 if (is_nil(metalist)) {
188 switch_goal(listhd(metalist));
193 function switch_goal(meta)
195 if (typeof meta == "undefined") {
196 goalview.innerHTML = "";
199 debug("switch_goal " + meta + "\n" + goalarray[meta]);
200 goalview.innerHTML = "<B>Goal ?" + meta + ":</B>\n\n" + goalarray[meta];
204 String.prototype.unescapeHTML = function()
206 var patt1 = /<br(\/|)>/gi;
207 var patt2 = /</gi;
208 var patt3 = />/gi;
210 result = result.replace(patt1,"\n");
211 result = result.replace(patt2,"<");
212 result = result.replace(patt3,">");
213 return (unescape(result));
218 advanceButton.disabled = true;
219 retractButton.disabled = true;
220 cursorButton.disabled = true;
221 bottomButton.disabled = true;
226 advanceButton.disabled = false;
227 retractButton.disabled = false;
228 cursorButton.disabled = false;
229 bottomButton.disabled = false;
232 function advanceForm1(cb)
236 if (window.XMLHttpRequest)
238 req = new XMLHttpRequest();
240 else if (window.ActiveXObject)
243 req = new ActiveXObject("Msxml2.XMLHTTP");
247 req = new ActiveXObject("Microsoft.XMLHTTP");
251 req.onreadystatechange = function()
256 stxt = req.statusText;
263 debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
264 response = req.responseText.split("@");
265 len = parseInt(response[0]);
266 len0 = unlocked.innerHTML.length;
267 unescaped = unlocked.innerHTML.unescapeHTML();
268 parsedtxt = unescaped.substr(0,len);
269 unparsedtxt = unescaped.substr(len);
270 locked.innerHTML = locked.innerHTML + parsedtxt;
271 unlocked.innerHTML = unparsedtxt;
272 len1 = unlocked.innerHTML.length;
274 populate_goalarray(response[1]);
275 statements = listcons(len2,statements);
276 unlocked.scrollIntoView(true);
280 debug("advance error: returned status code " + req.status + " " + req.statusText + "\n" +
290 req.open("POST", "advance"); // + escape(unlocked.innerHTML), true);
291 req.send(unlocked.innerHTML.unescapeHTML());
295 function gotoBottom()
299 if (window.XMLHttpRequest)
301 req = new XMLHttpRequest();
303 else if (window.ActiveXObject)
306 req = new ActiveXObject("Msxml2.XMLHTTP");
310 req = new ActiveXObject("Microsoft.XMLHTTP");
314 req.onreadystatechange = function()
319 stxt = req.statusText;
325 debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND");
326 response = req.responseText.split("@");
327 len = parseInt(response[0]);
328 len0 = unlocked.innerHTML.length;
329 unescaped = unlocked.innerHTML.unescapeHTML();
330 parsedtxt = unescaped.substr(0,len);
331 unparsedtxt = unescaped.substr(len);
332 locked.innerHTML = locked.innerHTML + parsedtxt;
333 unlocked.innerHTML = unparsedtxt;
334 len1 = unlocked.innerHTML.length;
336 populate_goalarray(response[1]);
337 statements = listcons(len,statements);
338 unlocked.scrollIntoView(true);
342 debug("goto bottom error: returned status code " + req.status + " " + req.statusText + "\n" +
348 req.open("POST", "bottom"); // + escape(unlocked.innerHTML), true);
349 req.send(unlocked.innerHTML.unescapeHTML());
353 function gotoPos(offset)
356 offset = getCursorPos();
359 advanceForm1(function(len) {
369 if (window.XMLHttpRequest)
371 req = new XMLHttpRequest();
373 else if (window.ActiveXObject)
376 req = new ActiveXObject("Msxml2.XMLHTTP");
380 req = new ActiveXObject("Microsoft.XMLHTTP");
384 req.onreadystatechange = function()
389 stxt = req.statusText;
395 debug("retract: received response\nBEGIN\n" + req.responseText + "\nEND");
396 response = req.responseText;
397 statementlen = parseInt(listhd(statements));
398 statements = listtl(statements);
399 lockedlen = locked.innerHTML.length - statementlen;
400 statement = locked.innerHTML.substr(lockedlen, statementlen);
401 locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
402 unlocked.innerHTML = statement + unlocked.innerHTML;
403 populate_goalarray(response);
404 unlocked.scrollIntoView(true);
408 debug("retract error: returned status code " + req.status + " " + req.statusText + "\n" +
414 req.open("GET", "retract"); // + escape(unlocked.innerHTML), true);
422 if (window.XMLHttpRequest)
424 req = new XMLHttpRequest();
426 else if (window.ActiveXObject)
429 req = new ActiveXObject("Msxml2.XMLHTTP");
433 req = new ActiveXObject("Microsoft.XMLHTTP");
437 req.onreadystatechange = function()
442 stxt = req.statusText;
448 locked.innerHTML = "";
449 unlocked.innerHTML = req.responseText;
453 debug("open error: returned status code " + req.status + " " + req.statusText + "\n" +
458 req.open("GET", "open?file=" + escape(filename.value), true);
464 function hideSequent() {
465 goalcell.parentNode.removeChild(goalcell);
466 scriptcell.setAttribute("colspan","2");
469 function showSequent() {
470 scriptcell.setAttribute("colspan","1");
471 workarea.appendChild(goalcell);
474 function removeElement(id) {
475 var element = document.getElementById(id);
476 element.parentNode.removeChild(element);
479 function getCursorPos() {
481 if (window.getSelection) {
482 var selObj = window.getSelection();
483 var selRange = selObj.getRangeAt(0);
484 //cursorPos = findNode(selObj.anchorNode.parentNode.childNodes, selObj.anchorNode) + selObj.anchorOffset;
485 cursorPos = findNode(unlocked.childNodes, selObj.anchorNode,0) + selObj.anchorOffset;
486 /* FIXME the following works wrong in Opera when the document is longer than 32767 chars */
489 else if (document.selection) {
490 var range = document.selection.createRange();
491 var bookmark = range.getBookmark();
492 /* FIXME the following works wrong when the document is longer than 65535 chars */
493 cursorPos = bookmark.charCodeAt(2) - 11; /* Undocumented function [3] */
498 function findNode(list, node, acc) {
499 for (var i = 0; i < list.length; i++) {
500 if (list[i] == node) {
501 // debug("success " + i);
504 if (list[i].hasChildNodes()) {
506 // debug("recursion on node " + i);
507 return (findNode(list[i].childNodes,node,acc))
509 catch (e) { /* debug("recursion failed"); */ }
511 sandbox = document.getElementById("sandbox");
512 dup = list[i].cloneNode(true);
513 sandbox.appendChild(dup);
514 // debug("fail " + i + ": " + sandbox.innerHTML);
515 acc += sandbox.innerHTML.length;
516 sandbox.removeChild(dup);
522 debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos()));
527 <body onLoad="initialize();">
528 <div id="sandbox" style="visibility:hidden;"></div>
529 <table style="table-layout: fixed; width:100%; height:100%; border-spacing: 0px; border-style: none;">
531 <td style="padding: 0px; width:67%; border-style: none;">
532 <textarea id="unescape" style="display:none;"></textarea>
533 <p><INPUT type="BUTTON" value="advance" id="advance" ONCLICK="advanceForm1()">
534 <INPUT type="BUTTON" value="go back" id="retract" ONCLICK="retract()">
535 <INPUT type="BUTTON" value="go to cursor" id="cursor" ONCLICK="gotoPos()">
536 <INPUT type="BUTTON" value="bottom" id="bottom" ONCLICK="gotoBottom()">
537 <INPUT type="TEXT" id="filename" value=""><INPUT type="BUTTON" value="Open" ONCLICK="openFile()"></p>
538 <INPUT type="BUTTON" value="show sequent" id="showseq" ONCLICK="showSequent()">
539 <INPUT type="BUTTON" value="hide sequent" id="hideseq" ONCLICK="hideSequent()">
540 <INPUT type="BUTTON" value="selection test" id="hideseq" ONCLICK="test()">
543 <td style="width:33%; text-align:center;"><img src="icons/matita-text.png"></td>
545 <tr id="workarea" style="height:80%;">
546 <td id="scriptcell" style="padding: 0px; border-style: none; padding: 0px;">
549 The two DIVs "locked" and "unlocked" MUST be on the same line (since they are
550 inside a PRE tag, a CR will be reflected in the document presentation)
552 <div style="width:100%; height:100%; overflow:auto;">
553 <pre><div contentEditable="false" id="locked" style="background-color:#bfbfff; display:inline;"></div><div contentEditable="true" id="unlocked" style="display:inline">(* script *)</div></pre></div>
554 <!-- the script (end) -->
556 <td id="goalcell" style="padding: 0px; width:33%; border-style: none;">
557 <div id="goals"></div>
558 <div contentEditable="true" style="border-style:solid; height:100%; width:100%; overflow:auto;">
559 <pre id="goalview"></pre>
563 <tr style="height:15%">
564 <td colspan="2" style="padding: 0px; border-style: none;">
565 <textarea id="logarea" style="width:100%; height:100%"></textarea>