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