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 dialogBox;
  15 var dialogTitle;
  16 var dialogContent;
  17 var metasenv = "";
  18 var lockedbackup = "";
  19
  20 function text_of_html(h)
  21 {
  22   if(document.all) {
  23      return h.innerText;
  24   } else {
  25      return h.textContent;
  26   }
  27 }
  28
  29 function unescape_html(s)
  30 {
  31   u = document.getElementById("unescape");
  32   u.innerHTML = s;
  33   return text_of_html(u)
  34 }
  35
  36 function initialize()
  37 {
  38   if (readCookie("session") == null) {
  39     window.location = "/login.html"
  40   } else {
  41     matitaTitle = document.getElementById("matitaTitle");
  42     locked = document.getElementById("locked");
  43     unlocked = document.getElementById("unlocked");
  44     workarea = document.getElementById("workarea");
  45     scriptcell = document.getElementById("scriptcell");
  46     goalcell = document.getElementById("goalcell");
  47     goals = document.getElementById("goals");
  48     goalview = document.getElementById("goalview");
  49     filename = document.getElementById("filename");
  50     logarea = document.getElementById("logarea");
  51     advanceButton = document.getElementById("advance");
  52     retractButton = document.getElementById("retract");
  53     cursorButton = document.getElementById("cursor");
  54     bottomButton = document.getElementById("bottom");
  55     dialogBox = document.getElementById("dialogBox");
  56     dialogTitle = document.getElementById("dialogTitle");
  57     dialogContent = document.getElementById("dialogContent");
  58
  59     changeFile("test.ma");
  60
  61     // hide sequent view at start
  62     hideSequent();
  63
  64     // initialize keyboard events in the unlocked script
  65     init_keyboard(unlocked);
  66   }
  67 }
  68
  69 function changeFile(name) {
  70     current_fname = name;
  71     matitaTitle.innerHTML = "Matita - cic:/matita/" + name;
  72 }
  73
  74 function init_keyboard(target)
  75 {
  76     if (target.addEventListener)
  77     {
  78 //       target.addEventListener("keydown",keydown,false);
  79        target.addEventListener("keypress",keypress,false);
  80 //       target.addEventListener("keyup",keyup,false);
  81 //       target.addEventListener("textInput",textinput,false);
  82     }
  83     else if (target.attachEvent)
  84     {
  85 //       target.attachEvent("onkeydown", keydown);
  86        target.attachEvent("onkeypress", keypress);
  87 //       target.attachEvent("onkeyup", keyup);
  88 //       target.attachEvent("ontextInput", textinput);
  89     }
  90     else
  91     {
  92 //       target.onkeydown= keydown;
  93        target.onkeypress= keypress;
  94 //       target.onkeyup= keyup;
  95 //       target.ontextinput= textinput;   // probably doesn't work
  96     }
  97
  98 }
  99
 100 function keyval(n)
 101 {
 102     if (n == null) return 'undefined';
 103     var s= '' + n;
 104     if (n >= 32 && n < 127) s+= ' (' + String.fromCharCode(n) + ')';
 105     while (s.length < 9) s+= ' ';
 106     return s;
 107 }
 108
 109 function string_of_key(n)
 110 {
 111     if (n == null) return 'undefined';
 112     return String.fromCharCode(n);
 113 }
 114
 115 function pressmesg(w,e)
 116 {
 117    debug(w + '  keyCode=' + keyval(e.keyCode) +
 118                  ' which=' + keyval(e.which) +
 119                  ' charCode=' + keyval(e.charCode) +
 120                  '\n          shiftKey='+e.shiftKey
 121               + ' ctrlKey='+e.ctrlKey
 122               + ' altKey='+e.altKey
 123               + ' metaKey='+e.metaKey);
 124 }
 125
 126 function suppressdefault(e,flag)
 127 {
 128    if (flag)
 129    {
 130        if (e.preventDefault) e.preventDefault();
 131        if (e.stopPropagation) e.stopPropagation();
 132    }
 133    return !flag;
 134 }
 135
 136 function restoreSelection(r) {
 137     unlocked.focus();
 138     if (r != null) {
 139         if (window.getSelection)//non IE and there is already a selection
 140         {
 141             var s = window.getSelection();
 142             if (s.rangeCount > 0)
 143                 s.removeAllRanges();
 144             s.addRange(r);
 145         }
 146         else
 147             if (document.createRange)//non IE and no selection
 148             {
 149                 window.getSelection().addRange(r);
 150             }
 151             else
 152                 if (document.selection)//IE
 153                 {
 154                     r.select();
 155                 }
 156     }
 157 }
 158
 159 function lookup_tex(texmacro)
 160 {
 161   texmacro = texmacro.substring(1);
 162   return unescape(macro2utf8[texmacro]);
 163 }
 164
 165 function keypress(e)
 166 {
 167    if (!e) e= event;
 168    pressmesg('keypress',e);
 169    var s = string_of_key(e.charCode);
 170    if (s == " ") {
 171         j = getCursorPos();
 172         i = unlocked.innerHTML.lastIndexOf('\\',j);
 173         if (i >= 0) {
 174           match = unlocked.innerHTML.substring(i,j);
 175           sym = unescape_html(lookup_tex(match));
 176           if (sym != "undefined") {
 177              if (window.getSelection) { // non IE
 178                 savedRange.setStart(savedsc,savedso - (j-i));
 179                 savedRange.deleteContents();
 180                 savedRange.insertNode(document.createTextNode(sym));
 181                 savedsc.parentNode.normalize();
 182                 if (savedRange.collapsed) { // Mozilla
 183                   savedRange.setEnd(savedsc,savedRange.endOffset + sym.length);
 184                 }
 185                 savedRange.collapse(false);
 186              } else {
 187                 savedRange.moveStart(i-j);
 188                 savedRange.text(sym);
 189                 savedRange.collapse(false);
 190              }
 191              restoreSelection(savedRange);
 192              return suppressdefault(e,true);
 193           }
 194           else {
 195              // restoreSelection(0);
 196              return suppressdefault(e,false);
 197           }
 198         }
 199         else return suppressdefault(e,false);
 200    } else {
 201         return suppressdefault(e,false);
 202    }
 203 }
 204
 205 var logtxt = "";
 206
 207 function debug(txt)
 208 {
 209         // internet explorer (v.9) doesn't work with innerHTML
 210         // but google chrome's innerText is, in a sense, "write only"
 211         // what should we do?
 212         // logarea.innerText = txt + "\n" + logarea.innerText;
 213         logtxt = logtxt + "\n" + txt;
 214 }
 215
 216 function showLog() {
 217   logWin = window.open( "", "Matita Log",
 218      "width=600,height=450,status,scrollbars,resizable,screenX=20,screenY=40,left=20,top=40");
 219   logWin.document.write('<html><head><title>Matita Log' + '</title></head>');
 220   logWin.document.write('<body><textarea style="width:100%;height:100%;">' +
 221     logtxt + '</textarea></body></html>');
 222   logWin.document.close();
 223 }
 224
 225 function listhd(l)
 226 {
 227         ar = l.split("#");
 228         debug("hd of '" + l + "' = '" + ar[0] + "'");
 229         return (ar[0]);
 230 }
 231
 232 function listtl(l)
 233 {
 234         i = l.indexOf("#");
 235         tl = l.substr(i+1);
 236         debug("tl of '" + l + "' = '" + tl + "'");
 237         return (tl);
 238 }
 239
 240 function listcons(x,l)
 241 {
 242         debug("cons '" + x + "' on '" + l + "'");
 243         return (x + "#" + l);
 244 }
 245
 246 function listnil()
 247 {
 248         return ("");
 249 }
 250
 251 function is_nil(l)
 252 {
 253         return (l == "");
 254 }
 255
 256 function fold_left (f,acc,l)
 257 {
 258         if (is_nil(l))
 259            { debug("'" + l + "' is fold end");
 260            return (acc); }
 261         else
 262            { debug("'" + l + "' is fold cons");
 263              return(fold_left (f,f(acc,(listhd(l))),listtl(l))); }
 264 }
 265
 266 function listiter (f,l)
 267 {
 268         if (is_nil(l))
 269         { debug("'" + l + "' is nil");
 270            return;
 271         }
 272         else
 273         {
 274            debug("'" + l + "' is not nil");
 275            f(listhd(l));
 276            listiter(f,listtl(l));
 277         }
 278 }
 279
 280 function listmap (f,l)
 281 {
 282         debug("listmap on " + l);
 283         if (is_nil(l))
 284            { debug("returning listnil");
 285              return(listnil());
 286            }
 287         else
 288            { debug("cons f(hd) map(f,tl)");
 289              return(f(listhd(l)) + "#" + listmap(f,listtl(l)));
 290            }
 291 }
 292
 293 var statements = listnil();
 294
 295 var goalarray;
 296 var metalist = listnil();
 297
 298 function pairmap (f,p)
 299 {
 300   debug("pairmap of '" + p + "'");
 301   ar = p.split("|");
 302   return (f(ar[0],ar[1]));
 303 }
 304
 305 function tripletmap (f,p)
 306 {
 307   debug("tripletmap of '" + p + "'");
 308   ar = p.split("|");
 309   return (f(ar[0],ar[1],ar[2]));
 310 }
 311
 312 function fst (p)
 313 {
 314   debug("fst");
 315   return (pairmap (function (a,b) { return (a); }, p));
 316 }
 317
 318 function p13 (p)
 319 {
 320   debug("p13");
 321   return (tripletmap (function (a,b,c) { return (a); }, p));
 322 }
 323
 324 function p23 (p)
 325 {
 326   debug("p23");
 327   return (tripletmap (function (a,b,c) { return (b); }, p));
 328 }
 329
 330 function p33 (p)
 331 {
 332   debug("f33");
 333   return (tripletmap (function (a,b,c) { return (c); }, p));
 334 }
 335
 336 function populate_goalarray(menv)
 337 {
 338   debug("metasenv.length = " + menv.length);
 339   if (menv.length == 0) {
 340       try {
 341           hideSequent();
 342       } catch (err) { };
 343   } else {
 344       showSequent();
 345       goalarray = new Array();
 346       metalist = listnil();
 347       var tmp_goallist = "";
 348       for (i = 0; i < menv.length; i++) {
 349         metano = menv[i].getAttribute("number");
 350         metaname = menv[i].childNodes[0].childNodes[0].data;
 351         goal = menv[i].childNodes[1].childNodes[0].data;
 352         debug ("found meta n. " + metano);
 353         debug ("found goal\nBEGIN" + goal + "\nEND");
 354         goalarray[metano] = goal;
 355         tmp_goallist = " <A href=\"javascript:switch_goal(" + metano + ")\">" + metaname + "</A>" + tmp_goallist;
 356         metalist = listcons(metano,metalist);
 357         debug ("goalarray[\"" + metano + "\"] = " + goalarray[metano]);
 358       }
 359       goals.innerHTML = tmp_goallist;
 360       debug("new metalist is '" + metalist + "'");
 361       if (is_nil(metalist)) {
 362         switch_goal();
 363       }
 364       else {
 365         switch_goal(listhd(metalist));
 366       }
 367   }
 368 }
 369
 370 function switch_goal(meta)
 371 {
 372   if (typeof meta == "undefined") {
 373     goalview.innerHTML = "";
 374   }
 375   else {
 376     debug("switch_goal " + meta + "\n" + goalarray[meta]);
 377     goalview.innerHTML = "<B>Goal ?" + meta + ":</B>\n\n" + goalarray[meta];
 378   }
 379 }
 380
 381 // the following is used to avoid escaping unicode, which results in
 382 // the server being unable to unescape the string
 383 String.prototype.sescape = function() {
 384         var patt1 = /%/gi;
 385         var patt2 = /=/gi;
 386         var patt3 = /&/gi;
 387         var patt4 = /\+/gi;
 388         var result = this;
 389         result = result.replace(patt1,"%25");
 390         result = result.replace(patt2,"%3D");
 391         result = result.replace(patt3,"%26");
 392         result = result.replace(patt4,"%2B");
 393         return (result);
 394 }
 395
 396 String.prototype.html_to_matita = function()
 397 {
 398         var patt1 = /<br(\/|)>/gi;
 399         var patt2 = /</gi
 400         var patt3 = />/gi
 401         var patt4 = /&lt;/gi;
 402         var patt5 = /&gt;/gi;
 403         var patt6 = /&nbsp;/gi;
 404         var result = this;
 405         result = result.replace(patt1,"\n");
 406         result = result.replace(patt2,"\005");
 407         result = result.replace(patt3,"\006");
 408         result = result.replace(patt4,"<");
 409         result = result.replace(patt5,">");
 410         result = result.replace(patt6," ");
 411         return (unescape(result));
 412 }
 413
 414 String.prototype.matita_to_html = function()
 415 {
 416         var patt1 = /</gi
 417         var patt2 = />/gi
 418         var patt3 = /\005/gi;
 419         var patt4 = /\006/gi;
 420         var result = this;
 421         result = result.replace(patt1,"&lt;");
 422         result = result.replace(patt2,"&gt;");
 423         result = result.replace(patt3,"<");
 424         result = result.replace(patt4,">");
 425         return (unescape(result));
 426 }
 427
 428 function pause()
 429 {
 430         advanceButton.disabled = true;
 431         retractButton.disabled = true;
 432         cursorButton.disabled = true;
 433         bottomButton.disabled = true;
 434 }
 435
 436 function resume()
 437 {
 438         advanceButton.disabled = false;
 439         retractButton.disabled = false;
 440         cursorButton.disabled = false;
 441         bottomButton.disabled = false;
 442 }
 443
 444 function is_defined(x)
 445 {
 446         return (typeof x != "undefined");
 447 }
 448
 449 /* servicename: name of the service being called
 450  * reqbody: text of the request
 451  * processResponse: processes the server response
 452  *     (takes the response text in input, undefined in case of error)
 453  */
 454 function callServer(servicename,processResponse,reqbody)
 455 {
 456         var req = null;
 457         // pause();
 458         if (window.XMLHttpRequest)
 459         {
 460                 req = new XMLHttpRequest();
 461         }
 462         else if (window.ActiveXObject)
 463         {
 464                 try {
 465                                 req = new ActiveXObject("Msxml2.XMLHTTP");
 466                 } catch (e)
 467                 {
 468                         try {
 469                                 req = new ActiveXObject("Microsoft.XMLHTTP");
 470                                 } catch (e) {}
 471                 }
 472         }
 473         req.onreadystatechange = function()
 474         {
 475
 476                 rs = req.readyState;
 477
 478                 if(rs == 4)
 479                 {
 480                         stat = req.status;
 481                         stxt = req.statusText;
 482                         if(stat == 200)
 483                         {
 484                           debug(req.responseText);
 485                           if (window.DOMParser) {
 486                             parser=new DOMParser();
 487                             xmlDoc=parser.parseFromString(req.responseText,"text/xml");
 488                           }
 489                           else // Internet Explorer
 490                           {
 491                             xmlDoc=new ActiveXObject("Microsoft.XMLDOM");
 492                             xmlDoc.async="false";
 493                             xmlDoc.loadXML(req.responseText);
 494                           }
 495                           processResponse(xmlDoc);
 496                         } else {
 497                           processResponse();
 498                         }
 499                 }
 500         };
 501         req.open("POST", servicename); // + escape(unlocked.innerHTML), true);
 502         req.setRequestHeader("Content-type","application/x-www-form-urlencoded");
 503         if (reqbody) {
 504                 req.send(reqbody);
 505         } else {
 506                 req.send();
 507         }
 508
 509 }
 510
 511 function advanceForm1()
 512 {
 513         processor = function(xml) {
 514                 if (is_defined(xml)) {
 515                         // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
 516                         parsed = xml.getElementsByTagName("parsed")[0];
 517                         len = parseInt(parsed.getAttribute("length"));
 518                         // len0 = unlocked.innerHTML.length;
 519                         unescaped = unlocked.innerHTML.html_to_matita();
 520                         parsedtxt = parsed.childNodes[0].nodeValue;
 521                         //parsedtxt = unescaped.substr(0,len);
 522                         unparsedtxt = unescaped.substr(len);
 523                         lockedbackup += parsedtxt;
 524                         locked.innerHTML = lockedbackup;
 525                         unlocked.innerHTML = unparsedtxt.matita_to_html();
 526                         // len1 = unlocked.innerHTML.length;
 527                         // len2 = len0 - len1;
 528                         len2 = parsedtxt.length;
 529                         metasenv = xml.getElementsByTagName("meta");
 530                         populate_goalarray(metasenv);
 531                         statements = listcons(len2,statements);
 532                         unlocked.scrollIntoView(true);
 533                 } else {
 534                         debug("advance failed");
 535                 }
 536                 resume();
 537         };
 538         pause();
 539         callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
 540
 541 }
 542
 543 function gotoBottom()
 544 {
 545         processor = function(xml) {
 546                 if (is_defined(xml)) {
 547                         // debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND");
 548                         parsed = xml.getElementsByTagName("parsed")[0];
 549                         len = parseInt(parsed.getAttribute("length"));
 550                         if (len > 0) {
 551                           // len0 = unlocked.innerHTML.length;
 552                           unescaped = unlocked.innerHTML.html_to_matita();
 553                           // not working in mozilla
 554                           // parsedtxt = parsed.childNodes[0].nodeValue;
 555                           parsedtxt = parsed.childNodes[0].wholeText;
 556                           //parsedtxt = unescaped.substr(0,len);
 557                           unparsedtxt = unescaped.substr(len);
 558                           lockedbackup += parsedtxt;
 559                           locked.innerHTML = lockedbackup; //.matita_to_html();
 560                           unlocked.innerHTML = unparsedtxt.matita_to_html();
 561                           // len1 = unlocked.innerHTML.length;
 562                           len2 = parsedtxt.length;
 563                           metasenv = xml.getElementsByTagName("meta");
 564                           populate_goalarray(metasenv);
 565                           if (len2 > 0)
 566                             statements = listcons(len2,statements);
 567                           unlocked.scrollIntoView(true);
 568                         }
 569                 } else {
 570                         debug("goto bottom failed");
 571                 }
 572                 resume();
 573         };
 574         pause();
 575         callServer("bottom",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
 576
 577 }
 578
 579
 580 function gotoTop()
 581 {
 582         processor = function(xml) {
 583                 if (is_defined(xml)) {
 584                   if (xml.childNodes[0].textContent != "ok") {
 585                      debug("goto top failed");
 586                   }
 587                   else
 588                         statements = listnil();
 589                         /*
 590                         lockedlen = locked.innerHTML.length - statementlen;
 591                         statement = locked.innerHTML.substr(lockedlen, statementlen);
 592                         locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
 593                         unlocked.innerHTML = statement + unlocked.innerHTML;
 594                         */
 595                         unlocked.innerHTML = lockedbackup + unlocked.innerHTML;
 596                         lockedbackup = "";
 597                         locked.innerHTML = lockedbackup;
 598                         hideSequent();
 599                         unlocked.scrollIntoView(true);
 600                 } else {
 601                         debug("goto top failed");
 602                 }
 603                 resume();
 604         };
 605         pause();
 606         callServer("top",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
 607
 608 }
 609 function gotoPos(offset)
 610 {
 611         if (!is_defined(offset)) {
 612                 offset = getCursorPos();
 613         }
 614         processor = function(xml) {
 615                 if (is_defined(xml)) {
 616                         parsed = xml.getElementsByTagName("parsed")[0];
 617                         len = parseInt(parsed.getAttribute("length"));
 618                         // len0 = unlocked.innerHTML.length;
 619                         unescaped = unlocked.innerHTML.html_to_matita();
 620                         parsedtxt = parsed.childNodes[0].nodeValue;
 621                         //parsedtxt = unescaped.substr(0,len);
 622                         unparsedtxt = unescaped.substr(len);
 623                         lockedbackup += parsedtxt;
 624                         locked.innerHTML = lockedbackup; //.matita_to_html();
 625                         unlocked.innerHTML = unparsedtxt.matita_to_html();
 626                         // len1 = unlocked.innerHTML.length;
 627                         len2 = parsedtxt.length;
 628                         metasenv = xml.getElementsByTagName("meta");
 629                         // populate_goalarray(metasenv);
 630                         statements = listcons(len2,statements);
 631                         unlocked.scrollIntoView(true);
 632                         // la populate non andrebbe fatta a ogni passo
 633                         if (offset <= len) {
 634                                 populate_goalarray(metasenv);
 635                                 resume();
 636                         } else {
 637                                 gotoPos(offset - len);
 638                         }
 639                 } else {
 640                         unlocked.scrollIntoView(true);
 641                         populate_goalarray(metasenv);
 642                         resume();
 643                 }
 644         }
 645         pause();
 646         callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
 647 }
 648
 649 function retract()
 650 {
 651         processor = function(xml) {
 652                 if (typeof xml != "undefined") {
 653                         // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
 654                         statementlen = parseInt(listhd(statements));
 655                         statements = listtl(statements);
 656                         /*
 657                         lockedlen = locked.innerHTML.length - statementlen;
 658                         statement = locked.innerHTML.substr(lockedlen, statementlen);
 659                         locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
 660                         unlocked.innerHTML = statement + unlocked.innerHTML;
 661                         */
 662                         lockedlen = lockedbackup.length - statementlen;
 663                         statement = lockedbackup.substr(lockedlen, statementlen);
 664                         lockedbackup = lockedbackup.substr(0,lockedlen);
 665                         locked.innerHTML = lockedbackup;
 666                         unlocked.innerHTML = statement + unlocked.innerHTML;
 667                         metasenv = xml.getElementsByTagName("meta");
 668                         populate_goalarray(metasenv);
 669                         unlocked.scrollIntoView(true);
 670                 } else {
 671                         debug("retract failed");
 672                 }
 673                 resume();
 674         };
 675         debug("retract 1");
 676         pause();
 677         callServer("retract",processor);
 678         debug("retract 2");
 679 }
 680
 681 function openFile()
 682 {
 683         processor = function(xml)
 684         {
 685                 if (is_defined(xml)) {
 686                         lockedbackup = "";
 687                         locked.innerHTML = lockedbackup;
 688                         unlocked.innerHTML = xml.documentElement.wholeText;
 689                 } else {
 690                         debug("file open failed");
 691                 }
 692         };
 693         callServer("open",processor,"file=" + escape(filename.value));
 694 }
 695
 696 function retrieveFile(thefile)
 697 {
 698         processor = function(xml)
 699         {
 700                 if (is_defined(xml)) {
 701                         changeFile(thefile);
 702                         lockedbackup = ""
 703                         locked.innerHTML = lockedbackup;
 704                         // code originally used in google chrome (problems with mozilla)
 705                         // debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
 706                         // unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
 707                         debug(xml.childNodes[0].textContent);
 708                         if (document.all) { // IE
 709                           unlocked.innerHTML = xml.childNodes[0].text;
 710                         } else {
 711                           unlocked.innerHTML = xml.childNodes[0].textContent;
 712                         }
 713
 714                 } else {
 715                         debug("file open failed");
 716                 }
 717         };
 718         dialogBox.style.display = "none";
 719         callServer("open",processor,"file=" + escape(thefile));
 720 }
 721
 722 function showLibrary(title,callback,reloadDialog)
 723 {
 724         var req = null;
 725         dialogBox.reload = reloadDialog;
 726         // pause();
 727         if (window.XMLHttpRequest)
 728         {
 729                 req = new XMLHttpRequest();
 730         }
 731         else if (window.ActiveXObject)
 732         {
 733                 try {
 734                                 req = new ActiveXObject("Msxml2.XMLHTTP");
 735                 } catch (e)
 736                 {
 737                         try {
 738                                 req = new ActiveXObject("Microsoft.XMLHTTP");
 739                                 } catch (e) {}
 740                 }
 741         }
 742         req.onreadystatechange = function()
 743         {
 744
 745                 rs = req.readyState;
 746
 747                 if(rs == 4)
 748                 {
 749                         stat = req.status;
 750                         stxt = req.statusText;
 751                         if(stat == 200)
 752                         {
 753                           debug(req.responseText);
 754                           showDialog("<H2>" + title + "</H2>",req.responseText, callback);
 755                         }
 756                 }
 757         };
 758         req.open("POST", "viewlib"); // + escape(unlocked.innerHTML), true);
 759         req.setRequestHeader("Content-type","application/x-www-form-urlencoded");
 760         req.send();
 761
 762 }
 763
 764 function uploadDialog()
 765 {
 766         uploadBox.style.display = "block";
 767 }
 768
 769 function uploadOK()
 770 {
 771    var file = document.getElementById("uploadFilename").files[0];
 772    if (file) {
 773        var filecontent = file.getAsText("UTF-8");
 774        locked.innerHTML = lockedbackup;
 775        unlocked.innerHTML = filecontent;
 776        uploadBox.style.display = "none";
 777    }
 778 //   if (file) {
 779 //      var reader = new FileReader();
 780 //      reader.readAsText(file, "UTF-8");
 781 //       reader.onloadend = function (evt) {
 782 //         lockedbackup = "";
 783 //           locked.innerHTML = lockedbackup
 784 //           unlocked.innerHTML = evt.target.result;
 785 //           uploadBox.style.display = "none";
 786 //       }
 787 //       reader.onerror = function (evt) {
 788 //         debug("file open failed");
 789 //           uploadBox.style.display = "none";
 790 //      }
 791 //   }
 792 }
 793
 794 function openDialog()
 795 {
 796         callback = function (fname) { retrieveFile(fname); };
 797         showLibrary("Open file", callback, openDialog);
 798 }
 799
 800 function saveDialog()
 801 {
 802         callback = function (fname) {
 803           dialogBox.style.display = "none";
 804           saveFile(fname,
 805                    (locked.innerHTML.html_to_matita()).sescape(),
 806                    (unlocked.innerHTML.html_to_matita()).sescape(),
 807                    false,saveDialog);
 808         };
 809         showLibrary("Save file as", callback, saveDialog);
 810 }
 811
 812 function newDialog()
 813 {
 814         callback = function (fname) {
 815           dialogBox.style.display = "none";
 816           saveFile(fname,"","",false,newDialog,true);
 817         };
 818         showLibrary("Create new file", callback, newDialog);
 819 }
 820
 821
 822 function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog,reloadFile)
 823 {
 824         if (!is_defined(reloadFile)) { reloadFile = true };
 825         if (!is_defined(fname)) {
 826             fname = current_fname;
 827             lockedtxt = (locked.innerHTML.html_to_matita()).sescape();
 828             unlockedtxt = (unlocked.innerHTML.html_to_matita()).sescape();
 829             force = true;
 830             // when force is true, reloadDialog is not needed
 831         }
 832         processor = function(xml) {
 833                 if (is_defined(xml)) {
 834                   if (xml.childNodes[0].textContent != "ok") {
 835                     if (confirm("File already exists. All existing data will be lost.\nDo you want to proceed anyway?")) {
 836                        saveFile(fname,lockedtxt,unlockedtxt,true,reloadDialog,reloadFile);
 837                     } else {
 838                       reloadDialog();
 839                     }
 840                   } else {
 841                     changeFile(fname);
 842                     debug("file saved!");
 843                     if (reloadFile) { retrieveFile(fname); }
 844                   }
 845                 } else {
 846                         debug("save file failed");
 847                 }
 848                 resume();
 849         };
 850         if (is_defined(fname)) {
 851           pause();
 852           callServer("save",processor,"file=" + escape(fname) +
 853                                     "&locked=" + lockedtxt +
 854                                     "&unlocked=" + unlockedtxt +
 855                                     "&force=" + force);
 856         }
 857         else { debug("no file selected"); }
 858 }
 859
 860 function createDir() {
 861    abortDialog();
 862    dirname = prompt("New directory name:\ncic:/matita/","newdir");
 863    if (dirname != null) {
 864         processor = function(xml) {
 865                 if (is_defined(xml)) {
 866                   if (xml.childNodes[0].textContent != "ok") {
 867                       alert("An error occurred :-(");
 868                   }
 869                 } else {
 870                       alert("An error occurred :-(");
 871                 }
 872                 dialogBox.reload();
 873         };
 874         pause();
 875         callServer("save",processor,"file=" + escape(dirname) +
 876                                     "&locked=&unlocked=&force=false&dir=true");
 877    } else {
 878       dialogBox.reload();
 879    }
 880 }
 881
 882 function commitAll()
 883 {
 884         processor = function(xml) {
 885                 if (is_defined(xml)) {
 886                         debug(xml.getElementsByTagName("details")[0].textContent);
 887                         alert("Commit executed: see details in the log.\n\n" +
 888                               "NOTICE: this message does NOT imply (yet) that the commit was successful.");
 889                 } else {
 890                         alert("Commit failed!");
 891                 }
 892                 resume();
 893         };
 894         pause();
 895         callServer("commit",processor);
 896 }
 897
 898 function updateAll()
 899 {
 900         processor = function(xml) {
 901                 if (is_defined(xml)) {
 902                         alert("Update executed.\n\n" +
 903                               "Details:\n" +
 904                               xml.getElementsByTagName("details")[0].textContent);
 905                 } else {
 906                         alert("Update failed!");
 907                 }
 908                 resume();
 909         };
 910         pause();
 911         callServer("update",processor);
 912 }
 913
 914 var goalcell;
 915
 916 function hideSequent() {
 917   goalcell.style.display = "none";
 918   scriptcell.style.width = "100%";
 919   scriptcell.style.minWidth = "100%";
 920   scriptcell.style.maxWidth = "100%";
 921 }
 922
 923 function showSequent() {
 924   scriptcell.style.width = "67%";
 925   scriptcell.style.minWidth = "67%";
 926   scriptcell.style.maxWidth = "67%";
 927   goalcell.style.display = "inline-block";
 928 }
 929
 930 function showDialog(title,content,callback) {
 931   dialogTitle.innerHTML = title;
 932   dialogContent.innerHTML = content;
 933   dialogBox.callback = callback;
 934   dialogBox.style.display = "block";
 935 }
 936
 937 function abortDialog() {
 938   dialogBox.style.display = "none";
 939 }
 940
 941 function abortUpload() {
 942   uploadBox.style.display = "none";
 943 }
 944
 945 function removeElement(id) {
 946   var element = document.getElementById(id);
 947   element.parentNode.removeChild(element);
 948 }
 949
 950 var savedsc;
 951 var savedso;
 952
 953 function getCursorPos() {
 954   var cursorPos;
 955   if (window.getSelection) {
 956     var selObj = window.getSelection();
 957     savedRange = selObj.getRangeAt(0);
 958     savedsc = savedRange.startContainer;
 959     savedso = savedRange.startOffset;
 960     //cursorPos =  findNode(selObj.anchorNode.parentNode.childNodes, selObj.anchorNode) + selObj.anchorOffset;
 961     cursorPos =  findNode(unlocked.childNodes, selObj.anchorNode,0) + selObj.anchorOffset;
 962     /* FIXME the following works wrong in Opera when the document is longer than 32767 chars */
 963     return(cursorPos);
 964   }
 965   else if (document.selection) {
 966     savedRange = document.selection.createRange();
 967     var bookmark = savedRange.getBookmark();
 968     /* FIXME the following works wrong when the document is longer than 65535 chars */
 969     cursorPos = bookmark.charCodeAt(2) - 11; /* Undocumented function [3] */
 970     return(cursorPos);
 971   }
 972 }
 973
 974 function findNode(list, node, acc) {
 975   for (var i = 0; i < list.length; i++) {
 976     if (list[i] == node) {
 977    //   debug("success " + i);
 978       return acc;
 979     }
 980     if (list[i].hasChildNodes()) {
 981        try {
 982    //      debug("recursion on node " + i);
 983          return (findNode(list[i].childNodes,node,acc))
 984        }
 985        catch (e) { /* debug("recursion failed"); */ }
 986     }
 987     sandbox = document.getElementById("sandbox");
 988     dup = list[i].cloneNode(true);
 989     sandbox.appendChild(dup);
 990 //    debug("fail " + i + ": " + sandbox.innerHTML);
 991     acc += sandbox.innerHTML.length;
 992     sandbox.removeChild(dup);
 993   }
 994   throw "not found";
 995 }
 996
 997 function test () {
 998   debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos()));
 999 }
1000
1001 function readCookie(name) {
1002         var nameEQ = name + "=";
1003         var ca = document.cookie.split(';');
1004         for(var i=0;i < ca.length;i++) {
1005                 var c = ca[i];
1006                 while (c.charAt(0)==' ') c = c.substring(1,c.length);
1007                 if (c.indexOf(nameEQ) == 0) return c.substring(nameEQ.length,c.length);
1008         }
1009         return null;
1010 }
1011
1012 function delete_cookie ( cookie_name )
1013 {
1014   var cookie_date = new Date();  // current date & time
1015   cookie_date.setTime ( cookie_date.getTime() - 1 );
1016   document.cookie = cookie_name += "=; expires=" + cookie_date.toGMTString();
1017 }
1018
1019 function delete_session()
1020 {
1021         delete_cookie("session");
1022 }