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