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