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