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.unescapeHTML = function()
 198 {
 199         var patt1 = /<br(\/|)>/gi;
 200         var patt2 = /&lt;/gi;
 201         var patt3 = /&gt;/gi;
 202         var result = this;
 203         result = result.replace(patt1,"\n");
 204         result = result.replace(patt2,"<");
 205         result = result.replace(patt3,">");
 206         return (unescape(result));
 207 }
 208
 209 function pause()
 210 {
 211         advanceButton.disabled = true;
 212         retractButton.disabled = true;
 213         cursorButton.disabled = true;
 214         bottomButton.disabled = true;
 215 }
 216
 217 function resume()
 218 {
 219         advanceButton.disabled = false;
 220         retractButton.disabled = false;
 221         cursorButton.disabled = false;
 222         bottomButton.disabled = false;
 223 }
 224
 225 function is_defined(x)
 226 {
 227         return (typeof x != "undefined");
 228 }
 229
 230 /* servicename: name of the service being called
 231  * reqbody: text of the request
 232  * processResponse: processes the server response
 233  *     (takes the response text in input, undefined in case of error)
 234  */
 235 function callServer(servicename,processResponse,reqbody)
 236 {
 237         var req = null;
 238         // pause();
 239         if (window.XMLHttpRequest)
 240         {
 241                 req = new XMLHttpRequest();
 242         }
 243         else if (window.ActiveXObject)
 244         {
 245                 try {
 246                                 req = new ActiveXObject("Msxml2.XMLHTTP");
 247                 } catch (e)
 248                 {
 249                         try {
 250                                 req = new ActiveXObject("Microsoft.XMLHTTP");
 251                                 } catch (e) {}
 252                 }
 253         }
 254         req.onreadystatechange = function()
 255         {
 256
 257                 rs = req.readyState;
 258
 259                 if(rs == 4)
 260                 {
 261                         stat = req.status;
 262                         stxt = req.statusText;
 263                         if(stat == 200)
 264                         {
 265                           debug(req.responseText);
 266                           if (window.DOMParser) {
 267                             parser=new DOMParser();
 268                             xmlDoc=parser.parseFromString(req.responseText,"text/xml");
 269                           }
 270                           else // Internet Explorer
 271                           {
 272                             xmlDoc=new ActiveXObject("Microsoft.XMLDOM");
 273                             xmlDoc.async="false";
 274                             xmlDoc.loadXML(req.responseText);
 275                           }
 276                           processResponse(xmlDoc);
 277                         } else {
 278                           processResponse();
 279                         }
 280                 }
 281         };
 282         req.open("POST", servicename); // + escape(unlocked.innerHTML), true);
 283         if (reqbody) {
 284                 req.send(reqbody);
 285         } else {
 286                 req.send();
 287         }
 288
 289 }
 290
 291 function advanceForm1()
 292 {
 293         processor = function(xml) {
 294                 if (is_defined(xml)) {
 295                         // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
 296                         len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length"));
 297                         len0 = unlocked.innerHTML.length;
 298                         unescaped = unlocked.innerHTML.unescapeHTML();
 299                         parsedtxt = unescaped.substr(0,len);
 300                         unparsedtxt = unescaped.substr(len);
 301                         locked.innerHTML = locked.innerHTML + parsedtxt;
 302                         unlocked.innerHTML = unparsedtxt;
 303                         len1 = unlocked.innerHTML.length;
 304                         len2 = len0 - len1;
 305                         metasenv = xml.getElementsByTagName("meta");
 306                         populate_goalarray(metasenv);
 307                         statements = listcons(len2,statements);
 308                         unlocked.scrollIntoView(true);
 309                 } else {
 310                         debug("advance failed");
 311                 }
 312                 resume();
 313         };
 314         pause();
 315         callServer("advance",processor,unlocked.innerHTML.unescapeHTML());
 316
 317 }
 318
 319 function gotoBottom()
 320 {
 321         processor = function(xml) {
 322                 if (is_defined(xml)) {
 323                         // debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND");
 324                         len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length"));
 325                         len0 = unlocked.innerHTML.length;
 326                         unescaped = unlocked.innerHTML.unescapeHTML();
 327                         parsedtxt = unescaped.substr(0,len);
 328                         unparsedtxt = unescaped.substr(len);
 329                         locked.innerHTML = locked.innerHTML + parsedtxt;
 330                         unlocked.innerHTML = unparsedtxt;
 331                         len1 = unlocked.innerHTML.length;
 332                         len2 = len0 - len1;
 333                         metasenv = xml.getElementsByTagName("meta");
 334                         populate_goalarray(metasenv);
 335                         statements = listcons(len2,statements);
 336                         unlocked.scrollIntoView(true);
 337                 } else {
 338                         debug("goto bottom failed");
 339                 }
 340                 resume();
 341         };
 342         pause();
 343         callServer("bottom",processor,unlocked.innerHTML.unescapeHTML());
 344
 345 }
 346
 347
 348 function gotoPos(offset)
 349 {
 350         if (!is_defined(offset)) {
 351                 offset = getCursorPos();
 352         }
 353         processor = function(xml) {
 354                 if (is_defined(xml)) {
 355                         // debug("goto pos: received response\nBEGIN\n" + req.responseText + "\nEND");
 356                         len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length"));
 357                         len0 = unlocked.innerHTML.length;
 358                         unescaped = unlocked.innerHTML.unescapeHTML();
 359                         parsedtxt = unescaped.substr(0,len);
 360                         unparsedtxt = unescaped.substr(len);
 361                         locked.innerHTML = locked.innerHTML + parsedtxt;
 362                         unlocked.innerHTML = unparsedtxt;
 363                         len1 = unlocked.innerHTML.length;
 364                         len2 = len0 - len1;
 365                         metasenv = xml.getElementsByTagName("meta");
 366                         // populate_goalarray(metasenv);
 367                         statements = listcons(len2,statements);
 368                         unlocked.scrollIntoView(true);
 369                         // la populate non andrebbe fatta a ogni passo
 370                         if (offset <= len) {
 371                                 populate_goalarray(metasenv);
 372                                 resume();
 373                         } else {
 374                                 gotoPos(offset - len);
 375                         }
 376                 } else {
 377                         unlocked.scrollIntoView(true);
 378                         populate_goalarray(metasenv);
 379                         resume();
 380                 }
 381         }
 382         pause();
 383         callServer("advance",processor,unlocked.innerHTML.unescapeHTML());
 384 }
 385
 386 function retract()
 387 {
 388         processor = function(xml) {
 389                 if (typeof xml != "undefined") {
 390                         // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
 391                         statementlen = parseInt(listhd(statements));
 392                         statements = listtl(statements);
 393                         lockedlen = locked.innerHTML.length - statementlen;
 394                         statement = locked.innerHTML.substr(lockedlen, statementlen);
 395                         locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
 396                         unlocked.innerHTML = statement + unlocked.innerHTML;
 397                         metasenv = xml.getElementsByTagName("meta");
 398                         populate_goalarray(metasenv);
 399                         unlocked.scrollIntoView(true);
 400                 } else {
 401                         debug("retract failed");
 402                 }
 403                 resume();
 404         };
 405         debug("retract 1");
 406         pause();
 407         callServer("retract",processor);
 408         debug("retract 2");
 409 }
 410
 411 function openFile()
 412 {
 413         processor = function(xml)
 414         {
 415                 if (is_defined(xml)) {
 416                         locked.innerHTML = "";
 417                         unlocked.innerHTML = xml.documentElement.firstChild.data;
 418                 } else {
 419                         debug("file open failed");
 420                 }
 421         };
 422         callServer("open?file=" + escape(filename.value),processor);
 423 }
 424
 425 var goalcell;
 426
 427 function hideSequent() {
 428   goalcell.parentNode.removeChild(goalcell);
 429   scriptcell.setAttribute("colspan","2");
 430 }
 431
 432 function showSequent() {
 433   scriptcell.setAttribute("colspan","1");
 434   workarea.appendChild(goalcell);
 435 }
 436
 437 function removeElement(id) {
 438   var element = document.getElementById(id);
 439   element.parentNode.removeChild(element);
 440 }
 441
 442 function getCursorPos() {
 443   var cursorPos;
 444   if (window.getSelection) {
 445     var selObj = window.getSelection();
 446     var selRange = selObj.getRangeAt(0);
 447     //cursorPos =  findNode(selObj.anchorNode.parentNode.childNodes, selObj.anchorNode) + selObj.anchorOffset;
 448     cursorPos =  findNode(unlocked.childNodes, selObj.anchorNode,0) + selObj.anchorOffset;
 449     /* FIXME the following works wrong in Opera when the document is longer than 32767 chars */
 450     return(cursorPos);
 451   }
 452   else if (document.selection) {
 453     var range = document.selection.createRange();
 454     var bookmark = range.getBookmark();
 455     /* FIXME the following works wrong when the document is longer than 65535 chars */
 456     cursorPos = bookmark.charCodeAt(2) - 11; /* Undocumented function [3] */
 457     return(cursorPos);
 458   }
 459 }
 460
 461 function findNode(list, node, acc) {
 462   for (var i = 0; i < list.length; i++) {
 463     if (list[i] == node) {
 464    //   debug("success " + i);
 465       return acc;
 466     }
 467     if (list[i].hasChildNodes()) {
 468        try {
 469    //      debug("recursion on node " + i);
 470          return (findNode(list[i].childNodes,node,acc))
 471        }
 472        catch (e) { /* debug("recursion failed"); */ }
 473     }
 474     sandbox = document.getElementById("sandbox");
 475     dup = list[i].cloneNode(true);
 476     sandbox.appendChild(dup);
 477 //    debug("fail " + i + ": " + sandbox.innerHTML);
 478     acc += sandbox.innerHTML.length;
 479     sandbox.removeChild(dup);
 480   }
 481   throw "not found";
 482 }
 483
 484 function test () {
 485   debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos()));
 486 }