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