matitaB/matita/matitaweb.js

   1 var locked;
   2 var unlocked;
   3 var workarea;
   4 var scriptcell;
   5 var goalcell;
   6 var goals;
   7 var goalview;
   8 var filename;
   9 var logarea;
  10 var advanceButton;
  11 var retractButton;
  12 var cursorButton;
  13 var bottomButton;
  14 var dialogBox;
  15 var dialogTitle;
  16 var dialogContent;
  17 var metasenv = "";
  18
  19 function initialize()
  20 {
  21   if (readCookie("session") == null) {
  22     window.location = "/login.html"
  23   } else {
  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");
  40
  41     // hide sequent view at start
  42     hideSequent();
  43
  44     // initialize keyboard events in the unlocked script
  45     init_keyboard(unlocked);
  46   }
  47 }
  48
  49 function init_keyboard(target)
  50 {
  51     if (target.addEventListener)
  52     {
  53 //       target.addEventListener("keydown",keydown,false);
  54        target.addEventListener("keypress",keypress,false);
  55 //       target.addEventListener("keyup",keyup,false);
  56 //       target.addEventListener("textInput",textinput,false);
  57     }
  58     else if (target.attachEvent)
  59     {
  60 //       target.attachEvent("onkeydown", keydown);
  61        target.attachEvent("onkeypress", keypress);
  62 //       target.attachEvent("onkeyup", keyup);
  63 //       target.attachEvent("ontextInput", textinput);
  64     }
  65     else
  66     {
  67 //       target.onkeydown= keydown;
  68        target.onkeypress= keypress;
  69 //       target.onkeyup= keyup;
  70 //       target.ontextinput= textinput;   // probably doesn't work
  71     }
  72
  73 }
  74
  75 function keyval(n)
  76 {
  77     if (n == null) return 'undefined';
  78     var s= '' + n;
  79     if (n >= 32 && n < 127) s+= ' (' + String.fromCharCode(n) + ')';
  80     while (s.length < 9) s+= ' ';
  81     return s;
  82 }
  83
  84 function string_of_key(n)
  85 {
  86     if (n == null) return 'undefined';
  87     return String.fromCharCode(n);
  88 }
  89
  90 function pressmesg(w,e)
  91 {
  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
  97               + ' altKey='+e.altKey
  98               + ' metaKey='+e.metaKey);
  99 }
 100
 101 function suppressdefault(e,flag)
 102 {
 103    if (flag)
 104    {
 105        if (e.preventDefault) e.preventDefault();
 106        if (e.stopPropagation) e.stopPropagation();
 107    }
 108    return !flag;
 109 }
 110
 111 function keypress(e)
 112 {
 113    if (!e) e= event;
 114    pressmesg('keypress',e);
 115    var s = string_of_key(e.charCode);
 116    if (s == " ") {
 117         j = getCursorPos();
 118         i = unlocked.innerHTML.lastIndexOf('\\',j);
 119         if (i >= 0) {
 120           match = unlocked.innerHTML.substring(i,j);
 121           pre = unlocked.innerHTML.substring(0,i-1);
 122           post = unlocked.innerHTML.substring(j+1);
 123           if (match == '\\to') {
 124              unlocked.innerHTML = pre + "-> " + post;
 125              return suppressdefault(e,true);
 126           }
 127           else return suppressdefault(e,false);
 128         }
 129         else return suppressdefault(e,false);
 130    } else {
 131         return suppressdefault(e,false);
 132    }
 133 }
 134
 135 function debug(txt)
 136 {
 137         // internet explorer (v.9) doesn't work with innerHTML
 138         // but google chrome's innerText is, in a sense, "write only"
 139         // what should we do?
 140         logarea.innerText = txt + "\n" + logarea.innerText;
 141 }
 142
 143 function listhd(l)
 144 {
 145         ar = l.split("#");
 146         debug("hd of '" + l + "' = '" + ar[0] + "'");
 147         return (ar[0]);
 148 }
 149
 150 function listtl(l)
 151 {
 152         i = l.indexOf("#");
 153         tl = l.substr(i+1);
 154         debug("tl of '" + l + "' = '" + tl + "'");
 155         return (tl);
 156 }
 157
 158 function listcons(x,l)
 159 {
 160         debug("cons '" + x + "' on '" + l + "'");
 161         return (x + "#" + l);
 162 }
 163
 164 function listnil()
 165 {
 166         return ("");
 167 }
 168
 169 function is_nil(l)
 170 {
 171         return (l == "");
 172 }
 173
 174 function fold_left (f,acc,l)
 175 {
 176         if (is_nil(l))
 177            { debug("'" + l + "' is fold end");
 178            return (acc); }
 179         else
 180            { debug("'" + l + "' is fold cons");
 181              return(fold_left (f,f(acc,(listhd(l))),listtl(l))); }
 182 }
 183
 184 function listiter (f,l)
 185 {
 186         if (is_nil(l))
 187         { debug("'" + l + "' is nil");
 188            return;
 189         }
 190         else
 191         {
 192            debug("'" + l + "' is not nil");
 193            f(listhd(l));
 194            listiter(f,listtl(l));
 195         }
 196 }
 197
 198 function listmap (f,l)
 199 {
 200         debug("listmap on " + l);
 201         if (is_nil(l))
 202            { debug("returning listnil");
 203              return(listnil());
 204            }
 205         else
 206            { debug("cons f(hd) map(f,tl)");
 207              return(f(listhd(l)) + "#" + listmap(f,listtl(l)));
 208            }
 209 }
 210
 211 var statements = listnil();
 212
 213 var goalarray;
 214 var metalist = listnil();
 215
 216 function pairmap (f,p)
 217 {
 218   debug("pairmap of '" + p + "'");
 219   ar = p.split("|");
 220   return (f(ar[0],ar[1]));
 221 }
 222
 223 function tripletmap (f,p)
 224 {
 225   debug("tripletmap of '" + p + "'");
 226   ar = p.split("|");
 227   return (f(ar[0],ar[1],ar[2]));
 228 }
 229
 230 function fst (p)
 231 {
 232   debug("fst");
 233   return (pairmap (function (a,b) { return (a); }, p));
 234 }
 235
 236 function p13 (p)
 237 {
 238   debug("p13");
 239   return (tripletmap (function (a,b,c) { return (a); }, p));
 240 }
 241
 242 function p23 (p)
 243 {
 244   debug("p23");
 245   return (tripletmap (function (a,b,c) { return (b); }, p));
 246 }
 247
 248 function p33 (p)
 249 {
 250   debug("f33");
 251   return (tripletmap (function (a,b,c) { return (c); }, p));
 252 }
 253
 254 function populate_goalarray(menv)
 255 {
 256   debug("metasenv.length = " + menv.length);
 257   if (menv.length == 0) {
 258       try {
 259           hideSequent();
 260       } catch (err) { };
 261   } else {
 262       showSequent();
 263       goalarray = new Array();
 264       metalist = listnil();
 265       var tmp_goallist = "";
 266       for (i = 0; i < menv.length; i++) {
 267         metano = menv[i].getAttribute("number");
 268         metaname = menv[i].childNodes[0].childNodes[0].data;
 269         goal = menv[i].childNodes[1].childNodes[0].data;
 270         debug ("found meta n. " + metano);
 271         debug ("found goal\nBEGIN" + goal + "\nEND");
 272         goalarray[metano] = goal;
 273         tmp_goallist = " <A href=\"javascript:switch_goal(" + metano + ")\">" + metaname + "</A>" + tmp_goallist;
 274         metalist = listcons(metano,metalist);
 275         debug ("goalarray[\"" + metano + "\"] = " + goalarray[metano]);
 276       }
 277       goals.innerHTML = tmp_goallist;
 278       debug("new metalist is '" + metalist + "'");
 279       if (is_nil(metalist)) {
 280         switch_goal();
 281       }
 282       else {
 283         switch_goal(listhd(metalist));
 284       }
 285   }
 286 }
 287
 288 function switch_goal(meta)
 289 {
 290   if (typeof meta == "undefined") {
 291     goalview.innerHTML = "";
 292   }
 293   else {
 294     debug("switch_goal " + meta + "\n" + goalarray[meta]);
 295     goalview.innerHTML = "<B>Goal ?" + meta + ":</B>\n\n" + goalarray[meta];
 296   }
 297 }
 298
 299 String.prototype.sescape = function() {
 300         var patt1 = /%/gi;
 301         var patt2 = /=/gi;
 302         var patt3 = /&/gi;
 303         var patt4 = /\+/gi;
 304         var result = this;
 305         result = result.replace(patt1,"%25");
 306         result = result.replace(patt2,"%3D");
 307         result = result.replace(patt3,"%26");
 308         result = result.replace(patt4,"%2B");
 309         return (result);
 310 }
 311
 312 String.prototype.unescapeHTML = function()
 313 {
 314         var patt1 = /<br(\/|)>/gi;
 315         var patt2 = /&lt;/gi;
 316         var patt3 = /&gt;/gi;
 317         var result = this;
 318         result = result.replace(patt1,"\n");
 319         result = result.replace(patt2,"<");
 320         result = result.replace(patt3,">");
 321         return (unescape(result));
 322 }
 323
 324 function pause()
 325 {
 326         advanceButton.disabled = true;
 327         retractButton.disabled = true;
 328         cursorButton.disabled = true;
 329         bottomButton.disabled = true;
 330 }
 331
 332 function resume()
 333 {
 334         advanceButton.disabled = false;
 335         retractButton.disabled = false;
 336         cursorButton.disabled = false;
 337         bottomButton.disabled = false;
 338 }
 339
 340 function is_defined(x)
 341 {
 342         return (typeof x != "undefined");
 343 }
 344
 345 /* servicename: name of the service being called
 346  * reqbody: text of the request
 347  * processResponse: processes the server response
 348  *     (takes the response text in input, undefined in case of error)
 349  */
 350 function callServer(servicename,processResponse,reqbody)
 351 {
 352         var req = null;
 353         // pause();
 354         if (window.XMLHttpRequest)
 355         {
 356                 req = new XMLHttpRequest();
 357         }
 358         else if (window.ActiveXObject)
 359         {
 360                 try {
 361                                 req = new ActiveXObject("Msxml2.XMLHTTP");
 362                 } catch (e)
 363                 {
 364                         try {
 365                                 req = new ActiveXObject("Microsoft.XMLHTTP");
 366                                 } catch (e) {}
 367                 }
 368         }
 369         req.onreadystatechange = function()
 370         {
 371
 372                 rs = req.readyState;
 373
 374                 if(rs == 4)
 375                 {
 376                         stat = req.status;
 377                         stxt = req.statusText;
 378                         if(stat == 200)
 379                         {
 380                           debug(req.responseText);
 381                           if (window.DOMParser) {
 382                             parser=new DOMParser();
 383                             xmlDoc=parser.parseFromString(req.responseText,"text/xml");
 384                           }
 385                           else // Internet Explorer
 386                           {
 387                             xmlDoc=new ActiveXObject("Microsoft.XMLDOM");
 388                             xmlDoc.async="false";
 389                             xmlDoc.loadXML(req.responseText);
 390                           }
 391                           processResponse(xmlDoc);
 392                         } else {
 393                           processResponse();
 394                         }
 395                 }
 396         };
 397         req.open("POST", servicename); // + escape(unlocked.innerHTML), true);
 398         req.setRequestHeader("Content-type","application/x-www-form-urlencoded");
 399         if (reqbody) {
 400                 req.send(reqbody);
 401         } else {
 402                 req.send();
 403         }
 404
 405 }
 406
 407 function advanceForm1()
 408 {
 409         processor = function(xml) {
 410                 if (is_defined(xml)) {
 411                         // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
 412                         len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length"));
 413                         len0 = unlocked.innerHTML.length;
 414                         unescaped = unlocked.innerHTML.unescapeHTML();
 415                         parsedtxt = unescaped.substr(0,len);
 416                         unparsedtxt = unescaped.substr(len);
 417                         locked.innerHTML = locked.innerHTML + parsedtxt;
 418                         unlocked.innerHTML = unparsedtxt;
 419                         len1 = unlocked.innerHTML.length;
 420                         len2 = len0 - len1;
 421                         metasenv = xml.getElementsByTagName("meta");
 422                         populate_goalarray(metasenv);
 423                         statements = listcons(len2,statements);
 424                         unlocked.scrollIntoView(true);
 425                 } else {
 426                         debug("advance failed");
 427                 }
 428                 resume();
 429         };
 430         pause();
 431         callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape());
 432
 433 }
 434
 435 function gotoBottom()
 436 {
 437         processor = function(xml) {
 438                 if (is_defined(xml)) {
 439                         // debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND");
 440                         len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length"));
 441                         len0 = unlocked.innerHTML.length;
 442                         unescaped = unlocked.innerHTML.unescapeHTML();
 443                         parsedtxt = unescaped.substr(0,len);
 444                         unparsedtxt = unescaped.substr(len);
 445                         locked.innerHTML = locked.innerHTML + parsedtxt;
 446                         unlocked.innerHTML = unparsedtxt;
 447                         len1 = unlocked.innerHTML.length;
 448                         len2 = len0 - len1;
 449                         metasenv = xml.getElementsByTagName("meta");
 450                         populate_goalarray(metasenv);
 451                         statements = listcons(len2,statements);
 452                         unlocked.scrollIntoView(true);
 453                 } else {
 454                         debug("goto bottom failed");
 455                 }
 456                 resume();
 457         };
 458         pause();
 459         callServer("bottom",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape());
 460
 461 }
 462
 463
 464 function gotoPos(offset)
 465 {
 466         if (!is_defined(offset)) {
 467                 offset = getCursorPos();
 468         }
 469         processor = function(xml) {
 470                 if (is_defined(xml)) {
 471                         // debug("goto pos: received response\nBEGIN\n" + req.responseText + "\nEND");
 472                         len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length"));
 473                         len0 = unlocked.innerHTML.length;
 474                         unescaped = unlocked.innerHTML.unescapeHTML();
 475                         parsedtxt = unescaped.substr(0,len);
 476                         unparsedtxt = unescaped.substr(len);
 477                         locked.innerHTML = locked.innerHTML + parsedtxt;
 478                         unlocked.innerHTML = unparsedtxt;
 479                         len1 = unlocked.innerHTML.length;
 480                         len2 = len0 - len1;
 481                         metasenv = xml.getElementsByTagName("meta");
 482                         // populate_goalarray(metasenv);
 483                         statements = listcons(len2,statements);
 484                         unlocked.scrollIntoView(true);
 485                         // la populate non andrebbe fatta a ogni passo
 486                         if (offset <= len) {
 487                                 populate_goalarray(metasenv);
 488                                 resume();
 489                         } else {
 490                                 gotoPos(offset - len);
 491                         }
 492                 } else {
 493                         unlocked.scrollIntoView(true);
 494                         populate_goalarray(metasenv);
 495                         resume();
 496                 }
 497         }
 498         pause();
 499         callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape());
 500 }
 501
 502 function retract()
 503 {
 504         processor = function(xml) {
 505                 if (typeof xml != "undefined") {
 506                         // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
 507                         statementlen = parseInt(listhd(statements));
 508                         statements = listtl(statements);
 509                         lockedlen = locked.innerHTML.length - statementlen;
 510                         statement = locked.innerHTML.substr(lockedlen, statementlen);
 511                         locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
 512                         unlocked.innerHTML = statement + unlocked.innerHTML;
 513                         metasenv = xml.getElementsByTagName("meta");
 514                         populate_goalarray(metasenv);
 515                         unlocked.scrollIntoView(true);
 516                 } else {
 517                         debug("retract failed");
 518                 }
 519                 resume();
 520         };
 521         debug("retract 1");
 522         pause();
 523         callServer("retract",processor);
 524         debug("retract 2");
 525 }
 526
 527 function openFile()
 528 {
 529         processor = function(xml)
 530         {
 531                 if (is_defined(xml)) {
 532                         locked.innerHTML = "";
 533                         unlocked.innerHTML = xml.documentElement.textContent;
 534                 } else {
 535                         debug("file open failed");
 536                 }
 537         };
 538         callServer("open",processor,"file=" + escape(filename.value));
 539 }
 540
 541 function retrieveFile(thefile)
 542 {
 543         processor = function(xml)
 544         {
 545                 if (is_defined(xml)) {
 546                         locked.innerHTML = "";
 547                         unlocked.innerHTML = xml.documentElement.textContent;
 548                 } else {
 549                         debug("file open failed");
 550                 }
 551         };
 552         dialogBox.style.display = "none";
 553         callServer("open",processor,"file=" + escape(thefile));
 554 }
 555
 556 function showLibrary()
 557 {
 558         var req = null;
 559         // pause();
 560         if (window.XMLHttpRequest)
 561         {
 562                 req = new XMLHttpRequest();
 563         }
 564         else if (window.ActiveXObject)
 565         {
 566                 try {
 567                                 req = new ActiveXObject("Msxml2.XMLHTTP");
 568                 } catch (e)
 569                 {
 570                         try {
 571                                 req = new ActiveXObject("Microsoft.XMLHTTP");
 572                                 } catch (e) {}
 573                 }
 574         }
 575         req.onreadystatechange = function()
 576         {
 577
 578                 rs = req.readyState;
 579
 580                 if(rs == 4)
 581                 {
 582                         stat = req.status;
 583                         stxt = req.statusText;
 584                         if(stat == 200)
 585                         {
 586                           debug(req.responseText);
 587                           showDialog("<H2>Library</H2>",req.responseText);
 588                         }
 589                 }
 590         };
 591         req.open("POST", "viewlib"); // + escape(unlocked.innerHTML), true);
 592         req.setRequestHeader("Content-type","application/x-www-form-urlencoded");
 593         req.send();
 594
 595 }
 596
 597 var goalcell;
 598
 599 function hideSequent() {
 600   goalcell.parentNode.removeChild(goalcell);
 601   scriptcell.setAttribute("colspan","2");
 602 }
 603
 604 function showSequent() {
 605   scriptcell.setAttribute("colspan","1");
 606   workarea.appendChild(goalcell);
 607 }
 608
 609 function showDialog(title,content) {
 610   dialogTitle.innerHTML = title;
 611   dialogContent.innerHTML = content;
 612   dialogBox.style.display = "block";
 613 }
 614
 615 function removeElement(id) {
 616   var element = document.getElementById(id);
 617   element.parentNode.removeChild(element);
 618 }
 619
 620 function getCursorPos() {
 621   var cursorPos;
 622   if (window.getSelection) {
 623     var selObj = window.getSelection();
 624     var selRange = selObj.getRangeAt(0);
 625     //cursorPos =  findNode(selObj.anchorNode.parentNode.childNodes, selObj.anchorNode) + selObj.anchorOffset;
 626     cursorPos =  findNode(unlocked.childNodes, selObj.anchorNode,0) + selObj.anchorOffset;
 627     /* FIXME the following works wrong in Opera when the document is longer than 32767 chars */
 628     return(cursorPos);
 629   }
 630   else if (document.selection) {
 631     var range = document.selection.createRange();
 632     var bookmark = range.getBookmark();
 633     /* FIXME the following works wrong when the document is longer than 65535 chars */
 634     cursorPos = bookmark.charCodeAt(2) - 11; /* Undocumented function [3] */
 635     return(cursorPos);
 636   }
 637 }
 638
 639 function findNode(list, node, acc) {
 640   for (var i = 0; i < list.length; i++) {
 641     if (list[i] == node) {
 642    //   debug("success " + i);
 643       return acc;
 644     }
 645     if (list[i].hasChildNodes()) {
 646        try {
 647    //      debug("recursion on node " + i);
 648          return (findNode(list[i].childNodes,node,acc))
 649        }
 650        catch (e) { /* debug("recursion failed"); */ }
 651     }
 652     sandbox = document.getElementById("sandbox");
 653     dup = list[i].cloneNode(true);
 654     sandbox.appendChild(dup);
 655 //    debug("fail " + i + ": " + sandbox.innerHTML);
 656     acc += sandbox.innerHTML.length;
 657     sandbox.removeChild(dup);
 658   }
 659   throw "not found";
 660 }
 661
 662 function test () {
 663   debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos()));
 664 }
 665
 666 function readCookie(name) {
 667         var nameEQ = name + "=";
 668         var ca = document.cookie.split(';');
 669         for(var i=0;i < ca.length;i++) {
 670                 var c = ca[i];
 671                 while (c.charAt(0)==' ') c = c.substring(1,c.length);
 672                 if (c.indexOf(nameEQ) == 0) return c.substring(nameEQ.length,c.length);
 673         }
 674         return null;
 675 }
 676
 677 function delete_cookie ( cookie_name )
 678 {
 679   var cookie_date = new Date();  // current date & time
 680   cookie_date.setTime ( cookie_date.getTime() - 1 );
 681   document.cookie = cookie_name += "=; expires=" + cookie_date.toGMTString();
 682 }
 683
 684 function delete_session()
 685 {
 686         delete_cookie("session");
 687 }