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