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