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