matitaB/matita/index.html

   1 <html>
   2 <head>
   3 </head>
   4
   5 <head>
   6 <script language="JavaScript">
   7 var locked;
   8 var unlocked;
   9 var workarea;
  10 var scriptcell;
  11 var goalcell;
  12 var goals;
  13 var goalview;
  14 var filename;
  15 var logarea;
  16 var advanceButton;
  17 var retractButton;
  18 var cursorButton;
  19 var bottomButton;
  20
  21 function initialize()
  22 {
  23   locked = document.getElementById("locked");
  24   unlocked = document.getElementById("unlocked");
  25   workarea = document.getElementById("workarea");
  26   scriptcell = document.getElementById("scriptcell");
  27   goalcell = document.getElementById("goalcell");
  28   goals = document.getElementById("goals");
  29   goalview = document.getElementById("goalview");
  30   filename = document.getElementById("filename");
  31   logarea = document.getElementById("logarea");
  32   advanceButton = document.getElementById("advance");
  33   retractButton = document.getElementById("retract");
  34   cursorButton = document.getElementById("cursor");
  35   bottomButton = document.getElementById("bottom");
  36
  37   // hide sequent view at start
  38   hideSequent();
  39 }
  40
  41 function debug(txt)
  42 {
  43         logarea.innerHTML = txt + "\n" + logarea.innerHTML;
  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(txt)
 158 {
 159   if (txt == "") {
 160       try {
 161           hideSequent();
 162       } catch (err) { };
 163   } else {
 164       showSequent();
 165       debug("populate with '" + txt + "'");
 166       goalarray = new Array();
 167       metalist = listnil();
 168       var tmp_goallist = "";
 169       listiter (function(item)
 170         {
 171          debug ("item is '" + item + "'");
 172          tripletmap (function(a,ahtml,b) {
 173           debug ("found meta n. " + a);
 174           debug ("found goal\nBEGIN" + unescape(b) + "\nEND");
 175           goalarray[a] = unescape(b);
 176           tmp_goallist = " <A href=\"javascript:switch_goal(" + a + ")\">" + unescape(ahtml) + "</A>" + tmp_goallist;
 177           metalist = listcons(a,metalist);
 178           debug ("goalarray[\"" + a + "\"] = " + goalarray[a]);
 179          },item);
 180         }, txt);
 181       // metalist = listmap (p13,txt);
 182       goals.innerHTML = tmp_goallist;
 183       debug("new metalist is '" + metalist + "'");
 184       if (is_nil(metalist)) {
 185         switch_goal();
 186       }
 187       else {
 188         switch_goal(listhd(metalist));
 189       }
 190   }
 191 }
 192
 193 function switch_goal(meta)
 194 {
 195   if (typeof meta == "undefined") {
 196     goalview.innerHTML = "";
 197   }
 198   else {
 199     debug("switch_goal " + meta + "\n" + goalarray[meta]);
 200     goalview.innerHTML = "<B>Goal ?" + meta + ":</B>\n\n" + goalarray[meta];
 201   }
 202 }
 203
 204 String.prototype.unescapeHTML = function()
 205 {
 206         var patt1 = /<br(\/|)>/gi;
 207         var patt2 = /&lt;/gi;
 208         var patt3 = /&gt;/gi;
 209         var result = this;
 210         result = result.replace(patt1,"\n");
 211         result = result.replace(patt2,"<");
 212         result = result.replace(patt3,">");
 213         return (unescape(result));
 214 }
 215
 216 function pause()
 217 {
 218         advanceButton.disabled = true;
 219         retractButton.disabled = true;
 220         cursorButton.disabled = true;
 221         bottomButton.disabled = true;
 222 }
 223
 224 function resume()
 225 {
 226         advanceButton.disabled = false;
 227         retractButton.disabled = false;
 228         cursorButton.disabled = false;
 229         bottomButton.disabled = false;
 230 }
 231
 232 function advanceForm1(cb)
 233 {
 234         var req = null;
 235         pause();
 236         if (window.XMLHttpRequest)
 237         {
 238                 req = new XMLHttpRequest();
 239         }
 240         else if (window.ActiveXObject)
 241         {
 242                 try {
 243                                 req = new ActiveXObject("Msxml2.XMLHTTP");
 244                 } catch (e)
 245                 {
 246                         try {
 247                                 req = new ActiveXObject("Microsoft.XMLHTTP");
 248                                 } catch (e) {}
 249                 }
 250         }
 251         req.onreadystatechange = function()
 252         {
 253
 254                 rs = req.readyState;
 255                 stat = req.status;
 256                 stxt = req.statusText;
 257
 258                 if(rs == 4)
 259                 {
 260                         var len;
 261                         if(stat == 200)
 262                         {
 263                                 debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
 264                                 response = req.responseText.split("@");
 265                                 len = parseInt(response[0]);
 266                                 len0 = unlocked.innerHTML.length;
 267                                 unescaped = unlocked.innerHTML.unescapeHTML();
 268                                 parsedtxt = unescaped.substr(0,len);
 269                                 unparsedtxt = unescaped.substr(len);
 270                                 locked.innerHTML = locked.innerHTML + parsedtxt;
 271                                 unlocked.innerHTML = unparsedtxt;
 272                                 len1 = unlocked.innerHTML.length;
 273                                 len2 = len0 - len1;
 274                                 populate_goalarray(response[1]);
 275                                 statements = listcons(len2,statements);
 276                                 unlocked.scrollIntoView(true);
 277                         }
 278                         else
 279                         {
 280                                 debug("advance error: returned status code " + req.status + " " + req.statusText + "\n" +
 281                                   req.responseText);
 282                                 len = 0;
 283                         }
 284                         resume();
 285                         if (cb) {
 286                                 cb(len);
 287                         }
 288                 }
 289         };
 290         req.open("POST", "advance"); // + escape(unlocked.innerHTML), true);
 291         req.send(unlocked.innerHTML.unescapeHTML());
 292
 293 }
 294
 295 function gotoBottom()
 296 {
 297         var req = null;
 298         pause();
 299         if (window.XMLHttpRequest)
 300         {
 301                 req = new XMLHttpRequest();
 302         }
 303         else if (window.ActiveXObject)
 304         {
 305                 try {
 306                                 req = new ActiveXObject("Msxml2.XMLHTTP");
 307                 } catch (e)
 308                 {
 309                         try {
 310                                 req = new ActiveXObject("Microsoft.XMLHTTP");
 311                                 } catch (e) {}
 312                 }
 313         }
 314         req.onreadystatechange = function()
 315         {
 316
 317                 rs = req.readyState;
 318                 stat = req.status;
 319                 stxt = req.statusText;
 320
 321                 if(rs == 4)
 322                 {
 323                         if(stat == 200)
 324                         {
 325                                 debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND");
 326                                 response = req.responseText.split("@");
 327                                 len = parseInt(response[0]);
 328                                 len0 = unlocked.innerHTML.length;
 329                                 unescaped = unlocked.innerHTML.unescapeHTML();
 330                                 parsedtxt = unescaped.substr(0,len);
 331                                 unparsedtxt = unescaped.substr(len);
 332                                 locked.innerHTML = locked.innerHTML + parsedtxt;
 333                                 unlocked.innerHTML = unparsedtxt;
 334                                 len1 = unlocked.innerHTML.length;
 335                                 len = len0 - len1;
 336                                 populate_goalarray(response[1]);
 337                                 statements = listcons(len,statements);
 338                                 unlocked.scrollIntoView(true);
 339                         }
 340                         else
 341                         {
 342                                 debug("goto bottom error: returned status code " + req.status + " " + req.statusText + "\n" +
 343                                   req.responseText);
 344                         }
 345                         resume();
 346                 }
 347         };
 348         req.open("POST", "bottom"); // + escape(unlocked.innerHTML), true);
 349         req.send(unlocked.innerHTML.unescapeHTML());
 350
 351 }
 352
 353 function gotoPos(offset)
 354 {
 355         if (!offset) {
 356                 offset = getCursorPos();
 357         }
 358         if (offset > 0) {
 359                 advanceForm1(function(len) {
 360                         gotoPos(offset-len)
 361                 });
 362         }
 363
 364 }
 365
 366 function retract()
 367 {
 368         var req = null;
 369         if (window.XMLHttpRequest)
 370         {
 371                 req = new XMLHttpRequest();
 372         }
 373         else if (window.ActiveXObject)
 374         {
 375                 try {
 376                                 req = new ActiveXObject("Msxml2.XMLHTTP");
 377                 } catch (e)
 378                 {
 379                         try {
 380                                 req = new ActiveXObject("Microsoft.XMLHTTP");
 381                                 } catch (e) {}
 382                 }
 383         }
 384         req.onreadystatechange = function()
 385         {
 386
 387                 rs = req.readyState;
 388                 stat = req.status;
 389                 stxt = req.statusText;
 390
 391                 if(rs == 4)
 392                 {
 393                         if(stat == 200)
 394                         {
 395                                 debug("retract: received response\nBEGIN\n" + req.responseText + "\nEND");
 396                                 response = req.responseText;
 397                                 statementlen = parseInt(listhd(statements));
 398                                 statements = listtl(statements);
 399                                 lockedlen = locked.innerHTML.length - statementlen;
 400                                 statement = locked.innerHTML.substr(lockedlen, statementlen);
 401                                 locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
 402                                 unlocked.innerHTML = statement + unlocked.innerHTML;
 403                                 populate_goalarray(response);
 404                                 unlocked.scrollIntoView(true);
 405                         }
 406                         else
 407                         {
 408                                 debug("retract error: returned status code " + req.status + " " + req.statusText + "\n" +
 409                                   req.responseText);
 410                         }
 411                         resume();
 412                 }
 413         };
 414         req.open("GET", "retract"); // + escape(unlocked.innerHTML), true);
 415         req.send();
 416
 417 }
 418
 419 function openFile()
 420 {
 421         var req = null;
 422         if (window.XMLHttpRequest)
 423         {
 424                 req = new XMLHttpRequest();
 425         }
 426         else if (window.ActiveXObject)
 427         {
 428                 try {
 429                                 req = new ActiveXObject("Msxml2.XMLHTTP");
 430                 } catch (e)
 431                 {
 432                         try {
 433                                 req = new ActiveXObject("Microsoft.XMLHTTP");
 434                                 } catch (e) {}
 435                 }
 436         }
 437         req.onreadystatechange = function()
 438         {
 439
 440                 rs = req.readyState;
 441                 stat = req.status;
 442                 stxt = req.statusText;
 443
 444                 if(rs == 4)
 445                 {
 446                         if(stat == 200)
 447                         {
 448                                 locked.innerHTML = "";
 449                                 unlocked.innerHTML = req.responseText;
 450                         }
 451                         else
 452                         {
 453                                 debug("open error: returned status code " + req.status + " " + req.statusText + "\n" +
 454                                   req.responseText);
 455                         }
 456                 }
 457         };
 458         req.open("GET", "open?file=" + escape(filename.value), true);
 459         req.send();
 460 }
 461
 462 var goalcell;
 463
 464 function hideSequent() {
 465   goalcell.parentNode.removeChild(goalcell);
 466   scriptcell.setAttribute("colspan","2");
 467 }
 468
 469 function showSequent() {
 470   scriptcell.setAttribute("colspan","1");
 471   workarea.appendChild(goalcell);
 472 }
 473
 474 function removeElement(id) {
 475   var element = document.getElementById(id);
 476   element.parentNode.removeChild(element);
 477 }
 478
 479 function getCursorPos() {
 480   var cursorPos;
 481   if (window.getSelection) {
 482     var selObj = window.getSelection();
 483     var selRange = selObj.getRangeAt(0);
 484     //cursorPos =  findNode(selObj.anchorNode.parentNode.childNodes, selObj.anchorNode) + selObj.anchorOffset;
 485     cursorPos =  findNode(unlocked.childNodes, selObj.anchorNode,0) + selObj.anchorOffset;
 486     /* FIXME the following works wrong in Opera when the document is longer than 32767 chars */
 487     return(cursorPos);
 488   }
 489   else if (document.selection) {
 490     var range = document.selection.createRange();
 491     var bookmark = range.getBookmark();
 492     /* FIXME the following works wrong when the document is longer than 65535 chars */
 493     cursorPos = bookmark.charCodeAt(2) - 11; /* Undocumented function [3] */
 494     return(cursorPos);
 495   }
 496 }
 497
 498 function findNode(list, node, acc) {
 499   for (var i = 0; i < list.length; i++) {
 500     if (list[i] == node) {
 501    //   debug("success " + i);
 502       return acc;
 503     }
 504     if (list[i].hasChildNodes()) {
 505        try {
 506    //      debug("recursion on node " + i);
 507          return (findNode(list[i].childNodes,node,acc))
 508        }
 509        catch (e) { /* debug("recursion failed"); */ }
 510     }
 511     sandbox = document.getElementById("sandbox");
 512     dup = list[i].cloneNode(true);
 513     sandbox.appendChild(dup);
 514 //    debug("fail " + i + ": " + sandbox.innerHTML);
 515     acc += sandbox.innerHTML.length;
 516     sandbox.removeChild(dup);
 517   }
 518   throw "not found";
 519 }
 520
 521 function test () {
 522   debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos()));
 523 }
 524 </script>
 525 </head>
 526
 527 <body onLoad="initialize();">
 528 <div id="sandbox" style="visibility:hidden;"></div>
 529 <table style="table-layout: fixed; width:100%; height:100%; border-spacing: 0px; border-style: none;">
 530 <tr>
 531 <td style="padding: 0px; width:67%; border-style: none;">
 532         <textarea id="unescape" style="display:none;"></textarea>
 533         <p><INPUT type="BUTTON" value="advance" id="advance" ONCLICK="advanceForm1()">
 534            <INPUT type="BUTTON" value="go back" id="retract" ONCLICK="retract()">
 535            <INPUT type="BUTTON" value="go to cursor" id="cursor" ONCLICK="gotoPos()">
 536            <INPUT type="BUTTON" value="bottom" id="bottom" ONCLICK="gotoBottom()"> &nbsp;
 537         <INPUT type="TEXT" id="filename" value=""><INPUT type="BUTTON" value="Open" ONCLICK="openFile()"></p>
 538            <INPUT type="BUTTON" value="show sequent" id="showseq" ONCLICK="showSequent()">
 539            <INPUT type="BUTTON" value="hide sequent" id="hideseq" ONCLICK="hideSequent()">
 540            <INPUT type="BUTTON" value="selection test" id="hideseq" ONCLICK="test()">
 541
 542 </td>
 543 <td style="width:33%; text-align:center;"><img src="icons/matita-text.png"></td>
 544 </tr>
 545 <tr id="workarea" style="height:80%;">
 546 <td id="scriptcell" style="padding: 0px; border-style: none; padding: 0px;">
 547   <!-- the script -->
 548   <!--
 549   The two DIVs "locked" and "unlocked" MUST be on the same line (since they are
 550   inside a PRE tag, a CR will be reflected in the document presentation)
 551   -->
 552   <div style="width:100%; height:100%; overflow:auto;">
 553   <pre><div contentEditable="false" id="locked" style="background-color:#bfbfff; display:inline;"></div><div contentEditable="true" id="unlocked" style="display:inline">(* script *)</div></pre></div>
 554   <!-- the script (end) -->
 555 </td>
 556 <td id="goalcell" style="padding: 0px; width:33%; border-style: none;">
 557   <div id="goals"></div>
 558   <div contentEditable="true" style="border-style:solid; height:100%; width:100%; overflow:auto;">
 559   <pre id="goalview"></pre>
 560   </div>
 561 </td>
 562
 563 <tr style="height:15%">
 564 <td colspan="2" style="padding: 0px; border-style: none;">
 565         <textarea id="logarea" style="width:100%; height:100%"></textarea>
 566 </td>
 567 </tr>
 568 </table>
 569  </body>
 570  </html>