matitaB/matita/index.html

   1 <html>
   2 <head>
   3 </head>
   4
   5 <body>
   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 status;
  16
  17 function initialize()
  18 {
  19   locked = document.getElementById("locked");
  20   unlocked = document.getElementById("unlocked");
  21   workarea = document.getElementById("workarea");
  22   scriptcell = document.getElementById("scriptcell");
  23   goalcell = document.getElementById("goalcell");
  24   goals = document.getElementById("goals");
  25   goalview = document.getElementById("goalview");
  26   filename = document.getElementById("filename");
  27   status = document.getElementById("status");
  28 }
  29
  30 function debug(txt)
  31 {
  32         var status = document.getElementById("status");
  33         status.innerHTML = txt + "\n" + status.innerHTML;
  34 }
  35
  36 function listhd(l)
  37 {
  38         ar = l.split("#");
  39         debug("hd of '" + l + "' = '" + ar[0] + "'");
  40         return (ar[0]);
  41 }
  42
  43 function listtl(l)
  44 {
  45         i = l.indexOf("#");
  46         tl = l.substr(i+1);
  47         debug("tl of '" + l + "' = '" + tl + "'");
  48         return (tl);
  49 }
  50
  51 function listcons(x,l)
  52 {
  53         debug("cons '" + x + "' on '" + l + "'");
  54         return (x + "#" + l);
  55 }
  56
  57 function listnil()
  58 {
  59         return ("");
  60 }
  61
  62 function is_nil(l)
  63 {
  64         return (l == "");
  65 }
  66
  67 function fold_left (f,acc,l)
  68 {
  69         if (is_nil(l))
  70            { debug("'" + l + "' is fold end");
  71            return (acc); }
  72         else
  73            { debug("'" + l + "' is fold cons");
  74              return(fold_left (f,f(acc,(listhd(l))),listtl(l))); }
  75 }
  76
  77 function listiter (f,l)
  78 {
  79         if (is_nil(l))
  80         { debug("'" + l + "' is nil");
  81            return;
  82         }
  83         else
  84         {
  85            debug("'" + l + "' is not nil");
  86            f(listhd(l));
  87            listiter(f,listtl(l));
  88         }
  89 }
  90
  91 function listmap (f,l)
  92 {
  93         debug("listmap on " + l);
  94         if (is_nil(l))
  95            { debug("returning listnil");
  96              return(listnil());
  97            }
  98         else
  99            { debug("cons f(hd) map(f,tl)");
 100              return(f(listhd(l)) + "#" + listmap(f,listtl(l)));
 101            }
 102 }
 103
 104 var statements = listnil();
 105
 106 var goalarray;
 107 var metalist = listnil();
 108
 109 function pairmap (f,p)
 110 {
 111   debug("pairmap of '" + p + "'");
 112   ar = p.split("|");
 113   return (f(ar[0],ar[1]));
 114 }
 115
 116 function tripletmap (f,p)
 117 {
 118   debug("tripletmap of '" + p + "'");
 119   ar = p.split("|");
 120   return (f(ar[0],ar[1],ar[2]));
 121 }
 122
 123 function fst (p)
 124 {
 125   debug("fst");
 126   return (pairmap (function (a,b) { return (a); }, p));
 127 }
 128
 129 function p13 (p)
 130 {
 131   debug("p13");
 132   return (tripletmap (function (a,b,c) { return (a); }, p));
 133 }
 134
 135 function p23 (p)
 136 {
 137   debug("p23");
 138   return (tripletmap (function (a,b,c) { return (b); }, p));
 139 }
 140
 141 function p33 (p)
 142 {
 143   debug("f33");
 144   return (tripletmap (function (a,b,c) { return (c); }, p));
 145 }
 146
 147 function populate_goalarray(txt)
 148 {
 149   debug("populate with '" + txt + "'");
 150   goalarray = new Array();
 151   metalist = listnil();
 152   var tmp_goallist = "";
 153   listiter (function(item)
 154     {
 155      debug ("item is '" + item + "'");
 156      tripletmap (function(a,ahtml,b) {
 157       debug ("found meta n. " + a);
 158       debug ("found goal\nBEGIN" + unescape(b) + "\nEND");
 159       goalarray[a] = unescape(b);
 160       tmp_goallist = " <A href=\"javascript:switch_goal(" + a + ")\">" + unescape(ahtml) + "</A>" + tmp_goallist;
 161       metalist = listcons(a,metalist);
 162       debug ("goalarray[\"" + a + "\"] = " + goalarray[a]);
 163      },item);
 164     }, txt);
 165   // metalist = listmap (p13,txt);
 166   document.getElementById("goals").innerHTML = tmp_goallist;
 167   debug("new metalist is '" + metalist + "'");
 168   if (is_nil(metalist)) {
 169     switch_goal();
 170   }
 171   else {
 172     switch_goal(listhd(metalist));
 173   }
 174 }
 175
 176 function switch_goal(meta)
 177 {
 178   goalview = document.getElementById("goalview");
 179   if (typeof meta == "undefined") {
 180     goalview.innerHTML = "";
 181   }
 182   else {
 183     debug("switch_goal " + meta + "\n" + goalarray[meta]);
 184     goalview.innerHTML = "<B>Goal ?" + meta + ":</B>\n\n" + goalarray[meta];
 185   }
 186 }
 187
 188 String.prototype.unescapeHTML = function()
 189 {
 190         var patt1 = /<br(\/|)>/gi;
 191         var patt2 = /&lt;/gi;
 192         var patt3 = /&gt;/gi;
 193         var result = this;
 194         result = result.replace(patt1,"\n");
 195         result = result.replace(patt2,"<");
 196         result = result.replace(patt3,">");
 197         return (unescape(result));
 198 }
 199
 200 function pause()
 201 {
 202         var advanceButton = document.getElementById("advance");
 203         var retractButton = document.getElementById("retract");
 204         advanceButton.disabled = true;
 205         retractButton.disabled = true;
 206 }
 207
 208 function resume()
 209 {
 210         var advanceButton = document.getElementById("advance");
 211         var retractButton = document.getElementById("retract");
 212         advanceButton.disabled = false;
 213         retractButton.disabled = false;
 214 }
 215
 216 function advanceForm1()
 217 {
 218         var req = null;
 219         unlocked = document.getElementById("unlocked");
 220         locked = document.getElementById("locked");
 221         goalview = document.getElementById("goalview");
 222         pause();
 223         if (window.XMLHttpRequest)
 224         {
 225                 req = new XMLHttpRequest();
 226         }
 227         else if (window.ActiveXObject)
 228         {
 229                 try {
 230                                 req = new ActiveXObject("Msxml2.XMLHTTP");
 231                 } catch (e)
 232                 {
 233                         try {
 234                                 req = new ActiveXObject("Microsoft.XMLHTTP");
 235                                 } catch (e) {}
 236                 }
 237         }
 238         req.onreadystatechange = function()
 239         {
 240
 241                 rs = req.readyState;
 242                 stat = req.status;
 243                 stxt = req.statusText;
 244
 245                 if(rs == 4)
 246                 {
 247                         if(stat == 200)
 248                         {
 249                                 debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
 250                                 response = req.responseText.split("@");
 251                                 len = parseInt(response[0]);
 252                                 len0 = unlocked.innerHTML.length;
 253                                 unescaped = unlocked.innerHTML.unescapeHTML();
 254                                 parsedtxt = unescaped.substr(0,len);
 255                                 unparsedtxt = unescaped.substr(len);
 256                                 locked.innerHTML = locked.innerHTML + parsedtxt;
 257                                 unlocked.innerHTML = unparsedtxt;
 258                                 len1 = unlocked.innerHTML.length;
 259                                 len = len0 - len1;
 260                                 populate_goalarray(response[1]);
 261                                 statements = listcons(len,statements);
 262                                 unlocked.scrollIntoView(true);
 263                         }
 264                         else
 265                         {
 266                                 debug("advance error: returned status code " + req.status + " " + req.statusText + "\n" +
 267                                   req.responseText);
 268                         }
 269                         resume();
 270                 }
 271         };
 272         req.open("POST", "advance"); // + escape(document.getElementById("unlocked").innerHTML), true);
 273         req.send(unlocked.innerHTML.unescapeHTML());
 274
 275 }
 276
 277 function retract()
 278 {
 279         var req = null;
 280         unlocked = document.getElementById("unlocked");
 281         locked = document.getElementById("locked");
 282         goalview = document.getElementById("goalview");
 283         if (window.XMLHttpRequest)
 284         {
 285                 req = new XMLHttpRequest();
 286         }
 287         else if (window.ActiveXObject)
 288         {
 289                 try {
 290                                 req = new ActiveXObject("Msxml2.XMLHTTP");
 291                 } catch (e)
 292                 {
 293                         try {
 294                                 req = new ActiveXObject("Microsoft.XMLHTTP");
 295                                 } catch (e) {}
 296                 }
 297         }
 298         req.onreadystatechange = function()
 299         {
 300
 301                 rs = req.readyState;
 302                 stat = req.status;
 303                 stxt = req.statusText;
 304
 305                 if(rs == 4)
 306                 {
 307                         if(stat == 200)
 308                         {
 309                                 debug("retract: received response\nBEGIN\n" + req.responseText + "\nEND");
 310                                 response = req.responseText;
 311                                 statementlen = parseInt(listhd(statements));
 312                                 statements = listtl(statements);
 313                                 lockedlen = locked.innerHTML.length - statementlen;
 314                                 statement = locked.innerHTML.substr(lockedlen, statementlen);
 315                                 locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
 316                                 unlocked.innerHTML = statement + unlocked.innerHTML;
 317                                 populate_goalarray(response);
 318                                 unlocked.scrollIntoView(true);
 319                         }
 320                         else
 321                         {
 322                                 debug("retract error: returned status code " + req.status + " " + req.statusText + "\n" +
 323                                   req.responseText);
 324                         }
 325                         resume();
 326                 }
 327         };
 328         req.open("GET", "retract"); // + escape(document.getElementById("unlocked").innerHTML), true);
 329         req.send();
 330
 331 }
 332
 333 function openFile()
 334 {
 335         unlocked = document.getElementById("unlocked");
 336         locked = document.getElementById("locked");
 337         var req = null;
 338         if (window.XMLHttpRequest)
 339         {
 340                 req = new XMLHttpRequest();
 341         }
 342         else if (window.ActiveXObject)
 343         {
 344                 try {
 345                                 req = new ActiveXObject("Msxml2.XMLHTTP");
 346                 } catch (e)
 347                 {
 348                         try {
 349                                 req = new ActiveXObject("Microsoft.XMLHTTP");
 350                                 } catch (e) {}
 351                 }
 352         }
 353         req.onreadystatechange = function()
 354         {
 355
 356                 rs = req.readyState;
 357                 stat = req.status;
 358                 stxt = req.statusText;
 359
 360                 if(rs == 4)
 361                 {
 362                         if(stat == 200)
 363                         {
 364                                 locked.innerHTML = "";
 365                                 unlocked.innerHTML = req.responseText;
 366                         }
 367                         else
 368                         {
 369                                 debug("open error: returned status code " + req.status + " " + req.statusText + "\n" +
 370                                   req.responseText);
 371                         }
 372                 }
 373         };
 374         req.open("GET", "open?file=" + escape(document.getElementById("filename").value), true);
 375         req.send();
 376 }
 377
 378 var goalcell;
 379
 380 function hideSequent() {
 381   goalcell = document.getElementById("goalcell");
 382   goalcell.parentNode.removeChild(goalcell);
 383   document.getElementById("scriptcell").setAttribute("colspan","2");
 384 }
 385
 386 function showSequent() {
 387   document.getElementById("scriptcell").setAttribute("colspan","1");
 388   document.getElementById("workarea").appendChild(goalcell);
 389 }
 390
 391 function removeElement(id) {
 392   var element = document.getElementById(id);
 393   element.parentNode.removeChild(element);
 394 }
 395
 396 </script>
 397
 398 <table style="table-layout: fixed; width:100%; height:100%; border-spacing: 0px; border-style: none;">
 399 <tr>
 400 <td style="padding: 0px; width:67%; border-style: none;">
 401         <textarea id="unescape" style="display:none;"></textarea>
 402         <p><INPUT type="BUTTON" value="advance" id="advance" ONCLICK="advanceForm1()">
 403            <INPUT type="BUTTON" value="go back" id="retract" ONCLICK="retract()"> &nbsp;
 404         <INPUT type="TEXT" id="filename" value=""><INPUT type="BUTTON" value="Open" ONCLICK="openFile()"></p>
 405            <INPUT type="BUTTON" value="show sequent" id="showseq" ONCLICK="showSequent()">
 406            <INPUT type="BUTTON" value="hide sequent" id="hideseq" ONCLICK="hideSequent()">
 407 </td>
 408 <td style="width:33%;"></td>
 409 </tr>
 410 <tr id="workarea" style="height:80%;">
 411 <td id="scriptcell" style="padding: 0px; border-style: none; padding: 0px;">
 412   <!-- the script -->
 413   <!--
 414   The two DIVs "locked" and "unlocked" MUST be on the same line (since they are
 415   inside a PRE tag, a CR will be reflected in the document presentation)
 416   -->
 417   <div style="width:100%; height:100%; overflow:auto;">
 418   <pre>
 419   <div contentEditable="false" id="locked" style="background-color:#bfbfff; display:inline;"></div><div contentEditable="true" id="unlocked" style="display:inline">(* script lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo *)</div></pre></div>
 420   <!-- the script (end) -->
 421 </td>
 422 <td id="goalcell" style="padding: 0px; width:33%; border-style: none;">
 423   <div id="goals"></div>
 424   <div contentEditable="true" style="border-style:solid; height:100%; width:100%; overflow:auto;">
 425   <pre id="goalview">lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo </pre>
 426   </div>
 427 </td>
 428
 429 <tr style="height:15%">
 430 <td colspan="2" style="padding: 0px; border-style: none;">
 431         <textarea id="status" style="width:100%; height:100%"></textarea>
 432 </td>
 433 </tr>
 434 </table>
 435  </body>
 436  </html>