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