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