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