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