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