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