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