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