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