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