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