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