matitaB/matita/html/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     matitaLayout = $('body').layout({
  53             applyDefaultStyles: true,
  54             north : {
  55                     closable: false,
  56                     resizable: false
  57             },
  58             east : {
  59                     onresize_end : resizeSide,
  60                     resizable : true,
  61                     size: int_of_px($('body').width())/3
  62             },
  63             south : {
  64                     closable: true,
  65                     resizable: true,
  66                     size: 80
  67             }
  68         });
  69     body = document.body;
  70     titlebar = document.getElementById("titlebar");
  71     matitaTitle = document.getElementById("matitaTitle");
  72     apparea = document.getElementById("matitaapparea");
  73     locked = document.getElementById("locked");
  74     unlocked = document.getElementById("unlocked");
  75     toparea = document.getElementById("toparea");
  76     workarea = document.getElementById("workarea");
  77     scriptcell = document.getElementById("scriptcell");
  78     sidearea = document.getElementById("sidearea");
  79     disambcell = document.getElementById("disambcell");
  80     goalcell = document.getElementById("goalcell");
  81     goals = document.getElementById("goals");
  82     goalview = document.getElementById("goalview");
  83     filename = document.getElementById("filename");
  84     logarea = document.getElementById("logarea");
  85     advanceButton = document.getElementById("advance");
  86     retractButton = document.getElementById("retract");
  87     cursorButton = document.getElementById("cursor");
  88     bottomButton = document.getElementById("bottom");
  89     dialogBox = document.getElementById("dialogBox");
  90     uploadBox = document.getElementById("uploadBox");
  91     dialogTitle = document.getElementById("dialogTitle");
  92     dialogContent = document.getElementById("dialogContent");
  93
  94     matita = new Object();
  95     matita.disambMode = matita.proofMode = false;
  96
  97     // hide sequent view at start
  98     initializeLayout();
  99     updateSide();
 100
 101     // hide log at start
 102     matitaLayout.hide("south");
 103
 104     // changeFile("test.ma");
 105     retrieveFile("test.ma");
 106
 107     // initialize keyboard events in the unlocked script
 108     init_keyboard(unlocked);
 109
 110     init_hyperlinks();
 111     init_autotraces();
 112
 113   }
 114 }
 115
 116 function go_hyperlink(atag) {
 117   var uri = atag.attr("href");
 118   var mybaseuri = uri.substring(0,uri.lastIndexOf('/'));
 119   var id = uri.substring(uri.lastIndexOf('/')+1,uri.lastIndexOf('.'));
 120   // only non-notations
 121   if (uri != "cic:/fakeuri.def(1)") {
 122      if (mybaseuri == baseuri) {
 123         try {
 124                 $('#'+id)[0].scrollIntoView(true);
 125         } catch (e) {
 126                 // best effort: if undefined, don't scroll
 127         }
 128      } else {
 129         createDocWin(mybaseuri,id);
 130      }
 131   }
 132   return false;
 133 }
 134
 135 function init_hyperlinks() {
 136   $("#unlocked a").click(function () { return go_hyperlink($(this))});
 137   $("#locked a").click(function () { return go_hyperlink($(this))});
 138   $("#goalview a").click(function () { return go_hyperlink($(this))});
 139 }
 140
 141 function init_autotraces() {
 142     $("#unlocked .autotactic").tooltip({
 143       delay: 0,
 144       showURL: false,
 145       bodyHandler: function() {
 146         return (trace_of($(this)[0]));
 147       }
 148     });
 149     $("#locked .autotactic").tooltip({
 150       delay: 0,
 151       showURL: false,
 152       bodyHandler: function() {
 153         return (trace_of($(this)[0]));
 154       }
 155     });
 156 }
 157
 158 function trace_of(node) {
 159   return text_of_html(filterByClass(node.childNodes,"autotrace")[0]);
 160 }
 161
 162 function changeFile(name) {
 163     current_fname = name;
 164     matitaTitle.innerHTML = "Matita - cic:/matita/" + name;
 165     baseuri = "cic:/matita/" + name.substring(0,name.lastIndexOf('.'));
 166 }
 167
 168 function init_keyboard(target)
 169 {
 170     if (target.addEventListener)
 171     {
 172 //       target.addEventListener("keydown",keydown,false);
 173        target.addEventListener("keypress",keypress,false);
 174 //       target.addEventListener("keyup",keyup,false);
 175 //       target.addEventListener("textInput",textinput,false);
 176     }
 177     else if (target.attachEvent)
 178     {
 179 //       target.attachEvent("onkeydown", keydown);
 180        target.attachEvent("onkeypress", keypress);
 181 //       target.attachEvent("onkeyup", keyup);
 182 //       target.attachEvent("ontextInput", textinput);
 183     }
 184     else
 185     {
 186 //       target.onkeydown= keydown;
 187        target.onkeypress= keypress;
 188 //       target.onkeyup= keyup;
 189 //       target.ontextinput= textinput;   // probably doesn't work
 190     }
 191
 192 }
 193
 194 function keyval(n)
 195 {
 196     if (n == null) return 'undefined';
 197     var s= '' + n;
 198     if (n >= 32 && n < 127) s+= ' (' + String.fromCharCode(n) + ')';
 199     while (s.length < 9) s+= ' ';
 200     return s;
 201 }
 202
 203 function string_of_key(n)
 204 {
 205     if (n == null) return 'undefined';
 206     return String.fromCharCode(n);
 207 }
 208
 209 function pressmesg(w,e)
 210 {
 211 /* for debugging only
 212    debug(w + '  keyCode=' + keyval(e.keyCode) +
 213                  ' which=' + keyval(e.which) +
 214                  ' charCode=' + keyval(e.charCode) +
 215                  '\n          shiftKey='+e.shiftKey
 216               + ' ctrlKey='+e.ctrlKey
 217               + ' altKey='+e.altKey
 218               + ' metaKey='+e.metaKey);
 219 */
 220 }
 221
 222 function suppressdefault(e,flag)
 223 {
 224    if (flag)
 225    {
 226        if (e.preventDefault) e.preventDefault();
 227        if (e.stopPropagation) e.stopPropagation();
 228    }
 229    return !flag;
 230 }
 231
 232 function restoreSelection(r) {
 233     unlocked.focus();
 234     if (r != null) {
 235         if (window.getSelection)//non IE and there is already a selection
 236         {
 237             var s = window.getSelection();
 238             if (s.rangeCount > 0)
 239                 s.removeAllRanges();
 240             s.addRange(r);
 241         }
 242         else
 243             if (document.createRange)//non IE and no selection
 244             {
 245                 window.getSelection().addRange(r);
 246             }
 247             else
 248                 if (document.selection)//IE
 249                 {
 250                     r.select();
 251                 }
 252     }
 253 }
 254
 255 function lookup_tex(texmacro)
 256 {
 257   texmacro = texmacro.substring(1);
 258   return unescape(macro2utf8[texmacro]);
 259 }
 260
 261 function strip_tags(tagname,classname)
 262 {
 263     var tags;
 264     if (is_defined(classname)) {
 265       tags = $(tagname + "." + classname);
 266     } else {
 267       tags = $(tagname);
 268     }
 269     var tlen = tags.length; // preserving the value from removeChild operations
 270     for (i = 0; i < tlen; i++) {
 271         var children = tags[i].childNodes;
 272         for (j = 0; j < children.length; j++) {
 273             tags[i].parentNode.insertBefore(children[j],tags[i]);
 274         }
 275     }
 276     tags.remove();
 277
 278     /*
 279
 280     var tags = unlocked.getElementsByTagName(tagname);
 281     if (is_defined(classname)) {
 282         tags = filterByClass(tags,classname);
 283     }
 284     var tlen = tags.length; // preserving the value from removeChild operations
 285     for (i = 0; i < tlen; i++) {
 286         var children = tags[i].childNodes;
 287         for (j = 0; j < children.length; j++) {
 288             tags[i].parentNode.insertBefore(children[j],tags[i]);
 289         }
 290     }
 291     for (var i = 0; i < tlen; i++) {
 292       tags[0].parentNode.removeChild(tags[0]);
 293     }
 294     */
 295 }
 296
 297 function strip_interpr() {
 298         pause();
 299         strip_tags("A");
 300         resume();
 301         // alert("strip_interpr ended");
 302 }
 303
 304 function strip_anchors() {
 305         strip_tags("INPUT","anchor");
 306 }
 307
 308 function keypress(e)
 309 {
 310    if (!e) e= event;
 311    pressmesg('keypress',e);
 312    var s = string_of_key(e.charCode);
 313    strip_tags("span","error");
 314    if (s == " ") {
 315         j = getCursorPos();
 316         i = unlocked.innerHTML.html_to_matita().lastIndexOf('\\',j);
 317         if (i >= 0) {
 318           match = unlocked.innerHTML.html_to_matita().substring(i,j);
 319           sym = unescape_html(lookup_tex(match));
 320           if (sym != "undefined") {
 321              if (window.getSelection) { // non IE
 322                 savedRange.setStart(savedsc,savedso - (j-i));
 323                 savedRange.deleteContents();
 324                 savedRange.insertNode(document.createTextNode(sym));
 325                 savedsc.parentNode.normalize();
 326                 if (savedRange.collapsed) { // Mozilla
 327                   savedRange.setEnd(savedsc,savedRange.endOffset + sym.length);
 328                 }
 329                 savedRange.collapse(false);
 330              } else {
 331                 savedRange.moveStart(i-j);
 332                 savedRange.text(sym);
 333                 savedRange.collapse(false);
 334              }
 335              restoreSelection(savedRange);
 336              return suppressdefault(e,true);
 337           }
 338           else {
 339              // restoreSelection(0);
 340              return suppressdefault(e,false);
 341           }
 342         }
 343         else return suppressdefault(e,false);
 344    } else {
 345         return suppressdefault(e,false);
 346    }
 347 }
 348
 349 var logtxt = "";
 350
 351 function debug(txt)
 352 {
 353         // internet explorer (v.9) doesn't work with innerHTML
 354         // but google chrome's innerText is, in a sense, "write only"
 355         // what should we do?
 356         // logarea.innerText = txt + "\n" + logarea.innerText;
 357         logtxt = /* logtxt + "\n" +*/ txt;
 358 }
 359
 360 function error(txt)
 361 {
 362         $('#bottomtext').children().first().text(txt);
 363         matitaLayout.show("south");
 364 }
 365
 366 function showLog() {
 367   var logWin = window.open( "", "Matita Log",
 368      "width=600,height=450,location=no,menubar=no,status=no,scrollbars,resizable,screenX=20,screenY=40,left=20,top=40");
 369   logWin.document.write('<html><head><title>Matita Log' + '</title></head>');
 370   logWin.document.write('<body><textarea style="width:100%;height:100%;">' +
 371     logtxt + '</textarea></body></html>');
 372   logWin.document.close();
 373 }
 374
 375 function listhd(l)
 376 {
 377         ar = l.split("#");
 378         debug("hd of '" + l + "' = '" + ar[0] + "'");
 379         return (ar[0]);
 380 }
 381
 382 function listtl(l)
 383 {
 384         i = l.indexOf("#");
 385         tl = l.substr(i+1);
 386         debug("tl of '" + l + "' = '" + tl + "'");
 387         return (tl);
 388 }
 389
 390 function listcons(x,l)
 391 {
 392         debug("cons '" + x + "' on '" + l + "'");
 393         return (x + "#" + l);
 394 }
 395
 396 function listnil()
 397 {
 398         return ("");
 399 }
 400
 401 function list_append(l1,l2)
 402 { return (l1 + l2) }
 403
 404 function is_nil(l)
 405 {
 406         return (l == "");
 407 }
 408
 409 function fold_left (f,acc,l)
 410 {
 411         if (is_nil(l))
 412            { debug("'" + l + "' is fold end");
 413            return (acc); }
 414         else
 415            { debug("'" + l + "' is fold cons");
 416              return(fold_left (f,f(acc,(listhd(l))),listtl(l))); }
 417 }
 418
 419 function listiter (f,l)
 420 {
 421         if (is_nil(l))
 422         { debug("'" + l + "' is nil");
 423            return;
 424         }
 425         else
 426         {
 427            debug("'" + l + "' is not nil");
 428            f(listhd(l));
 429            listiter(f,listtl(l));
 430         }
 431 }
 432
 433 function listmap (f,l)
 434 {
 435         debug("listmap on " + l);
 436         if (is_nil(l))
 437            { debug("returning listnil");
 438              return(listnil());
 439            }
 440         else
 441            { debug("cons f(hd) map(f,tl)");
 442              return(f(listhd(l)) + "#" + listmap(f,listtl(l)));
 443            }
 444 }
 445
 446 var statements = listnil();
 447
 448 var goalarray;
 449 var metalist = listnil();
 450
 451 function pairmap (f,p)
 452 {
 453   debug("pairmap of '" + p + "'");
 454   ar = p.split("|");
 455   return (f(ar[0],ar[1]));
 456 }
 457
 458 function tripletmap (f,p)
 459 {
 460   debug("tripletmap of '" + p + "'");
 461   ar = p.split("|");
 462   return (f(ar[0],ar[1],ar[2]));
 463 }
 464
 465 function fst (p)
 466 {
 467   debug("fst");
 468   return (pairmap (function (a,b) { return (a); }, p));
 469 }
 470
 471 function p13 (p)
 472 {
 473   debug("p13");
 474   return (tripletmap (function (a,b,c) { return (a); }, p));
 475 }
 476
 477 function p23 (p)
 478 {
 479   debug("p23");
 480   return (tripletmap (function (a,b,c) { return (b); }, p));
 481 }
 482
 483 function p33 (p)
 484 {
 485   debug("f33");
 486   return (tripletmap (function (a,b,c) { return (c); }, p));
 487 }
 488
 489 function populate_goalarray(menv)
 490 {
 491   debug("metasenv.length = " + menv.length);
 492   if (menv.length == 0) {
 493       try {
 494           hideSequent();
 495       } catch (err) { };
 496   } else {
 497       showSequent();
 498       goalarray = new Array();
 499       metalist = listnil();
 500       var tmp_goallist = "";
 501       for (i = 0; i < menv.length; i++) {
 502         metano = menv[i].getAttribute("number");
 503         // item 0 = <metaname>, item 1 = <goal>
 504         metaname = menv[i].childNodes[0].childNodes[0].wholeText;
 505         goal = menv[i].childNodes[1].childNodes[0].wholeText;
 506         debug ("found meta n. " + metano);
 507         debug ("found goal\nBEGIN" + goal + "\nEND");
 508         goalarray[metano] = goal;
 509         tmp_goallist = " <A href=\"javascript:switch_goal(" + metano + ")\">" + metaname + "</A>" + tmp_goallist;
 510         metalist = listcons(metano,metalist);
 511         debug ("goalarray[\"" + metano + "\"] = " + goalarray[metano]);
 512       }
 513       goals.innerHTML = tmp_goallist;
 514       debug("new metalist is '" + metalist + "'");
 515       if (is_nil(metalist)) {
 516         switch_goal();
 517       }
 518       else {
 519         switch_goal(listhd(metalist));
 520       }
 521   }
 522 }
 523
 524 function switch_goal(meta)
 525 {
 526   if (typeof meta == "undefined") {
 527     goalview.innerHTML = "";
 528   }
 529   else {
 530     debug("switch_goal " + meta + "\n" + goalarray[meta]);
 531     goalview.innerHTML = "<B>Goal ?" + meta + ":</B>\n\n" + goalarray[meta];
 532   }
 533 }
 534
 535 // the following is used to avoid escaping unicode, which results in
 536 // the server being unable to unescape the string
 537 String.prototype.sescape = function() {
 538         var patt1 = /%/gi;
 539         var patt2 = /=/gi;
 540         var patt3 = /&/gi;
 541         var patt4 = /\+/gi;
 542         var result = this;
 543         result = result.replace(patt1,"%25");
 544         result = result.replace(patt2,"%3D");
 545         result = result.replace(patt3,"%26");
 546         result = result.replace(patt4,"%2B");
 547         return (result);
 548 }
 549
 550 String.prototype.html_to_matita = function()
 551 {
 552         var patt1 = /<br(\/|)>/gi;
 553         var patt2 = /</gi
 554         var patt3 = />/gi
 555         var patt4 = /&lt;/gi;
 556         var patt5 = /&gt;/gi;
 557         var patt6 = /&nbsp;/gi;
 558         var result = this;
 559         result = result.replace(patt1,"\n");
 560         result = result.replace(patt2,"\005");
 561         result = result.replace(patt3,"\006");
 562         result = result.replace(patt4,"<");
 563         result = result.replace(patt5,">");
 564         result = result.replace(patt6," ");
 565         return (unescape(result));
 566 }
 567
 568 String.prototype.matita_to_html = function()
 569 {
 570         var patt1 = /</gi
 571         var patt2 = />/gi
 572         var patt3 = /\005/gi;
 573         var patt4 = /\006/gi;
 574         var result = this;
 575         result = result.replace(patt1,"&lt;");
 576         result = result.replace(patt2,"&gt;");
 577         result = result.replace(patt3,"<");
 578         result = result.replace(patt4,">");
 579         return (unescape(result));
 580 }
 581
 582 function is_defined(x)
 583 {
 584         return (typeof x != "undefined");
 585 }
 586
 587 /* servicename: name of the service being called
 588  * reqbody: text of the request
 589  * processResponse: processes the server response
 590  *     (takes the response text in input, undefined in case of error)
 591  */
 592 function callServer(servicename,processResponse,reqbody)
 593 {
 594         var req = null;
 595         // pause();
 596         if (window.XMLHttpRequest)
 597         {
 598                 req = new XMLHttpRequest();
 599         }
 600         else if (window.ActiveXObject)
 601         {
 602                 try {
 603                                 req = new ActiveXObject("Msxml2.XMLHTTP");
 604                 } catch (e)
 605                 {
 606                         try {
 607                                 req = new ActiveXObject("Microsoft.XMLHTTP");
 608                                 } catch (e) {}
 609                 }
 610         }
 611         req.onreadystatechange = function()
 612         {
 613
 614                 rs = req.readyState;
 615
 616                 if(rs == 4)
 617                 {
 618                         stat = req.status;
 619                         stxt = req.statusText;
 620                         if(stat == 200)
 621                         {
 622                           debug(req.responseText);
 623                           if (window.DOMParser) {
 624                             parser=new DOMParser();
 625                             xmlDoc=parser.parseFromString(req.responseText,"text/xml");
 626                           }
 627                           else // Internet Explorer
 628                           {
 629                             xmlDoc=new ActiveXObject("Microsoft.XMLDOM");
 630                             xmlDoc.async="false";
 631                             xmlDoc.loadXML(req.responseText);
 632                           }
 633                           processResponse(xmlDoc);
 634                         } else {
 635                           // in case of error, assume session has expired
 636                           window.location = "/login.html";
 637                           // processResponse();
 638                         }
 639                 }
 640         };
 641         req.open("POST", servicename); // + escape(unlocked.innerHTML), true);
 642         req.setRequestHeader("Content-type","application/x-www-form-urlencoded");
 643         if (reqbody) {
 644                 req.send(reqbody);
 645         } else {
 646                 req.send();
 647         }
 648
 649 }
 650
 651 function advOneStep(xml) {
 652         var parsed = xml.getElementsByTagName("parsed")[0];
 653         var ambiguity = xml.getElementsByTagName("ambiguity")[0];
 654         var disamberr = xml.getElementsByTagName("disamberror")[0];
 655         if (is_defined(parsed)) {
 656         // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
 657             var len = parseInt(parsed.getAttribute("length"));
 658             // len0 = unlocked.innerHTML.length;
 659             var unescaped = unlocked.innerHTML.html_to_matita();
 660             var parsedtxt = parsed.childNodes[0].wholeText;
 661             //parsedtxt = unescaped.substr(0,len);
 662             var unparsedtxt = unescaped.substr(len);
 663             lockedbackup += parsedtxt;
 664             locked.innerHTML = lockedbackup;
 665             unlocked.innerHTML = unparsedtxt.matita_to_html();
 666             // len1 = unlocked.innerHTML.length;
 667             // len2 = len0 - len1;
 668             var len2 = parsedtxt.length;
 669             metasenv = xml.getElementsByTagName("meta");
 670             statements = listcons(len2,statements);
 671             //unlocked.scrollIntoView(true);
 672             smartScroll();
 673             return len;
 674         }
 675         else if (is_defined(ambiguity)) {
 676             var start = parseInt(ambiguity.getAttribute("start"));
 677             var stop = parseInt(ambiguity.getAttribute("stop"));
 678             var choices = xml.getElementsByTagName("choice");
 679
 680             matita.ambiguityStart = start;
 681             matita.ambiguityStop = stop;
 682             matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
 683             matita.interpretations = [];
 684
 685             var unlockedtxt = unlocked.innerHTML.html_to_matita();
 686             var pre = unlockedtxt.substring(0,start).matita_to_html();
 687             var mid = unlockedtxt.substring(start,stop).matita_to_html();
 688             var post = unlockedtxt.substring(stop).matita_to_html();
 689             unlocked.innerHTML = pre +
 690                     "<span class=\"error\" title=\"disambiguation error\">" +
 691                     mid + "</span>" + post;
 692
 693             var title = "<H3>Ambiguous input</H3>";
 694             disambcell.innerHTML = title;
 695             for (i = 0;i < choices.length;i++) {
 696                 matita.interpretations[i] = new Object();
 697
 698                 var href = choices[i].getAttribute("href");
 699                 var title = choices[i].getAttribute("title");
 700                 var desc = choices[i].childNodes[0].nodeValue;
 701
 702                 matita.interpretations[i].href = href;
 703                 matita.interpretations[i].title = title;
 704                 matita.interpretations[i].desc = desc;
 705
 706                 var choice = document.createElement("input");
 707                 choice.setAttribute("type","radio");
 708                 choice.setAttribute("name","interpr");
 709                 choice.setAttribute("href",href);
 710                 choice.setAttribute("title",title);
 711                 if (i == 0) choice.setAttribute("checked","");
 712
 713                 disambcell.appendChild(choice);
 714                 disambcell.appendChild(document.createTextNode(desc));
 715                 disambcell.appendChild(document.createElement("br"));
 716             }
 717
 718             var okbutton = document.createElement("input");
 719             okbutton.setAttribute("type","button");
 720             okbutton.setAttribute("value","OK");
 721             okbutton.setAttribute("onclick","do_disambiguate()");
 722             var cancelbutton = document.createElement("input");
 723             cancelbutton.setAttribute("type","button");
 724             cancelbutton.setAttribute("value","Cancel");
 725             cancelbutton.setAttribute("onclick","cancel_disambiguate()");
 726
 727             disambcell.appendChild(okbutton);
 728             disambcell.appendChild(cancelbutton);
 729
 730             matita.disambMode = true;
 731             updateSide();
 732             throw "Stop";
 733         }
 734         else if (is_defined(disamberr)) {
 735             // must be fixed in a daemon: it makes sense to return a
 736             // disambiguation error with no choices
 737             if (disamberr.childNodes.length > 0) {
 738               set_cps(disamberr.childNodes);
 739               matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
 740               matita.disambMode = true;
 741               next_cp(0);
 742             }
 743             throw "Stop";
 744         }
 745         else {
 746             var error = xml.getElementsByTagName("error")[0];
 747             unlocked.innerHTML = error.childNodes[0].wholeText;
 748             error(xml.childNodes[0].nodeValue);
 749             throw "Stop";
 750         }
 751
 752 }
 753
 754 function advanceForm1()
 755 {
 756         processor = function(xml) {
 757            try {
 758                 if (is_defined(xml)) {
 759                     advOneStep(xml);
 760                     populate_goalarray(metasenv);
 761                     init_hyperlinks();
 762                     init_autotraces();
 763                 } else {
 764                         error("advance failed");
 765                 }
 766             } catch (e) {
 767                     // nothing to do
 768             };
 769             resume();
 770         };
 771         pause();
 772         callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
 773
 774 }
 775
 776 // get or set <choicepoint>'s (in case of disamb error)
 777 function get_cps() {
 778         return matita.choicepoints
 779 }
 780
 781 function set_cps(cps) {
 782         matita.choicepoints = cps;
 783 }
 784
 785 // get radio buttons for <choice>'s in a given cp
 786 function get_choice_opts(i) {
 787    var res = [];
 788    var choices = get_cps()[i].childNodes;
 789    for (var j = 0;j < choices.length;j++) {
 790       var href = choices[j].getAttribute("href");
 791       var title = choices[j].getAttribute("title");
 792       var desc;
 793       if (is_defined(title) && title != null) {
 794            desc = title;
 795       } else if (is_defined(href) && href != null) {
 796            desc = href;
 797       } else {
 798            desc = null;
 799       }
 800
 801       res[j] = document.createElement("input");
 802       res[j].setAttribute("type","radio");
 803       res[j].setAttribute("name","choice");
 804       res[j].setAttribute("choicepointno",i);
 805       res[j].setAttribute("choiceno",j);
 806       res[j].setAttribute("href",href);
 807       res[j].setAttribute("title",title);
 808       if (desc != null) res[j].setAttribute("desc",desc);
 809
 810       if (j == 0) res[j].setAttribute("checked","");
 811   }
 812   return res;
 813 }
 814
 815 // get radio buttons for <failure>'s in a given choice
 816 function get_failure_opts(i,j) {
 817    var res = [];
 818    var failures = get_cps()[i].childNodes[j].childNodes;
 819    for (var k = 0;k < failures.length;k++) {
 820       var start = failures[k].getAttribute("start");
 821       var stop = failures[k].getAttribute("stop");
 822       var title = failures[k].getAttribute("title");
 823
 824       res[k] = document.createElement("input");
 825       res[k].setAttribute("type","radio");
 826       res[k].setAttribute("name","failure");
 827       res[k].setAttribute("choicepointno",i);
 828       res[k].setAttribute("choiceno",j);
 829       res[k].setAttribute("failureno",k);
 830       res[k].setAttribute("start",start);
 831       res[k].setAttribute("stop",stop);
 832       res[k].setAttribute("title",title);
 833
 834       if (k == 0) res[k].setAttribute("checked","");
 835   }
 836   return res;
 837 }
 838
 839 function next_cp(curcp) {
 840         var cp = get_cps()[curcp];
 841         var start = parseInt(cp.getAttribute("start"));
 842         var stop = parseInt(cp.getAttribute("stop"));
 843
 844         matita.errorStart = start;
 845         matita.errorStop = stop;
 846         // matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
 847
 848         var unlockedtxt = matita.unlockedbackup;
 849         var pre = unlockedtxt.substring(0,start).matita_to_html();
 850         var mid = unlockedtxt.substring(start,stop).matita_to_html();
 851         var post = unlockedtxt.substring(stop).matita_to_html();
 852         unlocked.innerHTML = pre +
 853                 "<span class=\"error\" title=\"error location\">" +
 854                 mid + "</span>" + post;
 855
 856         var title = "<H3>Error diagnostics</H3>";
 857         disambcell.innerHTML = title;
 858         var choices = get_choice_opts(curcp);
 859         for (var i = 0;i < choices.length;i++) {
 860             disambcell.appendChild(choices[i]);
 861             var desc = choices[i].getAttribute("desc");
 862             if (!is_defined(desc) || desc == null) {
 863                     desc = "Interpretation " + i;
 864             }
 865             disambcell.appendChild(document.createTextNode(desc));
 866             disambcell.appendChild(document.createElement("br"));
 867         }
 868
 869         // update index of the next choicepoint
 870         new_curcp = (curcp + 1) % get_cps().length;
 871
 872         var okbutton = document.createElement("input");
 873         okbutton.setAttribute("type","button");
 874         okbutton.setAttribute("value","OK");
 875         okbutton.setAttribute("onclick","show_failures()");
 876         var cancelbutton = document.createElement("input");
 877         cancelbutton.setAttribute("type","button");
 878         cancelbutton.setAttribute("value","Close");
 879         cancelbutton.setAttribute("onclick","cancel_disambiguate()");
 880         var tryagainbutton = document.createElement("input");
 881         tryagainbutton.setAttribute("type","button");
 882         if (new_curcp > 0) {
 883             tryagainbutton.setAttribute("value","Try something else");
 884         } else {
 885             tryagainbutton.setAttribute("value","Restart");
 886         }
 887         tryagainbutton.setAttribute("onclick","next_cp(" + new_curcp + ")");
 888
 889         disambcell.appendChild(okbutton);
 890         disambcell.appendChild(tryagainbutton);
 891         disambcell.appendChild(cancelbutton);
 892
 893         //disable_toparea();
 894
 895         //matita.disambMode = true;
 896         updateSide();
 897
 898 }
 899
 900 function show_failures() {
 901
 902         var choice = document.getElementsByName("choice")[get_checked_index("choice")];
 903         var cpno = parseInt(choice.getAttribute("choicepointno"));
 904         var choiceno = parseInt(choice.getAttribute("choiceno"));
 905         var choicedesc = choice.getAttribute("desc");
 906
 907         var title = "<H3>Error diagnostics</H3>";
 908         var subtitle;
 909         if (is_defined(choicedesc) && choicedesc != null) {
 910                 subtitle  = "<p>Errors at node " + cpno + " = " + choicedesc + "</p>";
 911         } else {
 912                 subtitle = "<p>Global errors:</p>";
 913         }
 914
 915         disambcell.innerHTML = title + subtitle;
 916         var failures = get_failure_opts(cpno,choiceno);
 917         for (var i = 0;i < failures.length;i++) {
 918             disambcell.appendChild(failures[i]);
 919             disambcell.appendChild(document.createTextNode(failures[i].getAttribute("title")));
 920             disambcell.appendChild(document.createElement("br"));
 921         }
 922
 923         var okbutton = document.createElement("input");
 924         okbutton.setAttribute("type","button");
 925         okbutton.setAttribute("value","Show error loc");
 926         okbutton.setAttribute("onclick","show_err()");
 927         var cancelbutton = document.createElement("input");
 928         cancelbutton.setAttribute("type","button");
 929         cancelbutton.setAttribute("value","Close");
 930         cancelbutton.setAttribute("onclick","cancel_disambiguate()");
 931         var backbutton = document.createElement("input");
 932         backbutton.setAttribute("type","button");
 933         backbutton.setAttribute("value","<< Back");
 934         backbutton.setAttribute("onclick","next_cp(" + cpno + ")");
 935
 936         disambcell.appendChild(backbutton);
 937         disambcell.appendChild(okbutton);
 938         disambcell.appendChild(cancelbutton);
 939
 940 }
 941
 942 function show_err() {
 943         var radios = document.getElementsByName("failure");
 944         for (i = 0; i < radios.length; i++) {
 945             if (radios[i].checked) {
 946                 var start = radios[i].getAttribute("start");
 947                 var stop = radios[i].getAttribute("stop");
 948                 var title = radios[i].getAttribute("title");
 949                 var unlockedtxt = matita.unlockedbackup;
 950                 var pre = unlockedtxt.substring(0,start).matita_to_html();
 951                 var mid = unlockedtxt.substring(start,stop).matita_to_html();
 952                 var post = unlockedtxt.substring(stop).matita_to_html();
 953                 unlocked.innerHTML = pre +
 954                         "<span class=\"error\" title=\"Disambiguation failure\">" +
 955                         mid + "</span>" + post;
 956                 break;
 957             }
 958         }
 959 }
 960
 961 function gotoBottom()
 962 {
 963         processor = function(xml) {
 964                 if (is_defined(xml)) {
 965                         // debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND");
 966                         var parsed = xml.getElementsByTagName("parsed");
 967                         var localized = xml.getElementsByTagName("localized")[0];
 968                         var ambiguity = xml.getElementsByTagName("ambiguity")[0];
 969                         var generic_err = xml.getElementsByTagName("error")[0];
 970                         var disamberr = xml.getElementsByTagName("disamberror")[0];
 971                         for (var i = 0;i < parsed.length; i++) {
 972                           var len = parsed[i].getAttribute("length");
 973                           // len0 = unlocked.innerHTML.length;
 974                           var unescaped = unlocked.innerHTML.html_to_matita();
 975                           // the browser may decide to split textnodes: use wholeText!
 976                           var parsedtxt = parsed[i].childNodes[0].wholeText;
 977                           //parsedtxt = unescaped.substr(0,len);
 978                           var unparsedtxt = unescaped.substr(len);
 979                           lockedbackup += parsedtxt;
 980                           locked.innerHTML = lockedbackup; //.matita_to_html();
 981                           unlocked.innerHTML = unparsedtxt.matita_to_html();
 982                           // len1 = unlocked.innerHTML.length;
 983                           var len2 = parsedtxt.length;
 984                           statements = listcons(len2,statements);
 985                         }
 986                         // unlocked.scrollIntoView(true);
 987                         smartScroll();
 988                         metasenv = xml.getElementsByTagName("meta");
 989                         init_hyperlinks();
 990                         init_autotraces();
 991                         populate_goalarray(metasenv);
 992
 993                         if (is_defined(ambiguity)) {
 994                             var start = parseInt(ambiguity.getAttribute("start"));
 995                             var stop = parseInt(ambiguity.getAttribute("stop"));
 996                             var choices = xml.getElementsByTagName("choice");
 997
 998                             matita.ambiguityStart = start;
 999                             matita.ambiguityStop = stop;
1000                             matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
1001                             matita.interpretations = [];
1002
1003                             var unlockedtxt = unlocked.innerHTML.html_to_matita();
1004                             var pre = unlockedtxt.substring(0,start).matita_to_html();
1005                             var mid = unlockedtxt.substring(start,stop).matita_to_html();
1006                             var post = unlockedtxt.substring(stop).matita_to_html();
1007                             unlocked.innerHTML = pre +
1008                                     "<span class=\"error\" title=\"disambiguation error\">" +
1009                                     mid + "</span>" + post;
1010
1011                             var title = "<H3>Ambiguous input</H3>";
1012                             disambcell.innerHTML = title;
1013                             for (i = 0;i < choices.length;i++) {
1014                                 matita.interpretations[i] = new Object();
1015
1016                                 var href = choices[i].getAttribute("href");
1017                                 var title = choices[i].getAttribute("title");
1018                                 var desc = choices[i].childNodes[0].nodeValue;
1019
1020                                 matita.interpretations[i].href = href;
1021                                 matita.interpretations[i].title = title;
1022                                 matita.interpretations[i].desc = desc;
1023
1024                                 var choice = document.createElement("input");
1025                                 choice.setAttribute("type","radio");
1026                                 choice.setAttribute("name","interpr");
1027                                 choice.setAttribute("href",href);
1028                                 choice.setAttribute("title",title);
1029                                 if (i == 0) choice.setAttribute("checked","");
1030
1031                                 disambcell.appendChild(choice);
1032                                 disambcell.appendChild(document.createTextNode(desc));
1033                                 disambcell.appendChild(document.createElement("br"));
1034                             }
1035
1036                             var okbutton = document.createElement("input");
1037                             okbutton.setAttribute("type","button");
1038                             okbutton.setAttribute("value","OK");
1039                             okbutton.setAttribute("onclick","do_disambiguate()");
1040                             var cancelbutton = document.createElement("input");
1041                             cancelbutton.setAttribute("type","button");
1042                             cancelbutton.setAttribute("value","Cancel");
1043                             cancelbutton.setAttribute("onclick","cancel_disambiguate()");
1044
1045                             disambcell.appendChild(okbutton);
1046                             disambcell.appendChild(cancelbutton);
1047
1048                             matita.disambMode = true;
1049                             updateSide();
1050                         }
1051                         else if (is_defined(disamberr)) {
1052                             // must be fixed in a daemon: it makes sense to return a
1053                             // disambiguation error with no choices
1054                             if (disamberr.childNodes.length > 0) {
1055                               set_cps(disamberr.childNodes);
1056                               matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
1057                               matita.disambMode = true;
1058                               next_cp(0);
1059                             }
1060                             throw "Stop";
1061                         }
1062                         else if (is_defined(localized)) {
1063                             unlocked.innerHTML = localized.childNodes[0].wholeText;
1064                         }
1065                         else if (is_defined(generic_err)) {
1066                             error("Unmanaged error:\n" + generic_err.childNodes[0].wholeText);
1067                         }
1068                 } else {
1069                         error("goto bottom failed");
1070                 }
1071                 resume();
1072         };
1073         pause();
1074         callServer("bottom",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
1075 }
1076
1077
1078 function gotoTop()
1079 {
1080         processor = function(xml) {
1081                 if (is_defined(xml)) {
1082                   if (xml.childNodes[0].textContent != "ok") {
1083                      error("goto top failed");
1084                   }
1085                   else
1086                         statements = listnil();
1087                         /*
1088                         lockedlen = locked.innerHTML.length - statementlen;
1089                         statement = locked.innerHTML.substr(lockedlen, statementlen);
1090                         locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
1091                         unlocked.innerHTML = statement + unlocked.innerHTML;
1092                         */
1093                         unlocked.innerHTML = lockedbackup + unlocked.innerHTML;
1094                         lockedbackup = "";
1095                         locked.innerHTML = lockedbackup;
1096                         init_hyperlinks();
1097                         init_autotraces();
1098                         hideSequent();
1099                         strip_anchors();
1100                         // unlocked.scrollIntoView(true);
1101                         smartScroll();
1102                 } else {
1103                         error("goto top failed");
1104                 }
1105                 resume();
1106         };
1107         pause();
1108         callServer("top",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
1109
1110 }
1111
1112 function gotoPos(offset)
1113 {
1114         if (!is_defined(offset)) {
1115                 offset = getCursorPos();
1116         }
1117         processor = function(xml) {
1118                 if (is_defined(xml)) {
1119                     try {
1120                         var len = advOneStep(xml);
1121                         if (offset <= len) {
1122                                 init_hyperlinks();
1123                                 init_autotraces();
1124                                 populate_goalarray(metasenv);
1125                                 resume();
1126                         } else {
1127                                 gotoPos(offset - len);
1128                         }
1129                     } catch (er) {
1130                         init_hyperlinks();
1131                         init_autotraces();
1132                         populate_goalarray(metasenv);
1133                         resume();
1134                     }
1135                 } else {
1136                         init_hyperlinks();
1137                         init_autotraces();
1138                         // unlocked.scrollIntoView(true);
1139                         smartScroll();
1140                         populate_goalarray(metasenv);
1141                         resume();
1142                 }
1143         }
1144         pause();
1145         callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
1146 }
1147
1148 function retractStep()
1149 {
1150         processor = function(xml) {
1151                 if (typeof xml != "undefined") {
1152                         // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
1153                         statementlen = parseInt(listhd(statements));
1154                         statements = listtl(statements);
1155                         /*
1156                         lockedlen = locked.innerHTML.length - statementlen;
1157                         statement = locked.innerHTML.substr(lockedlen, statementlen);
1158                         locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
1159                         unlocked.innerHTML = statement + unlocked.innerHTML;
1160                         */
1161                         lockedlen = lockedbackup.length - statementlen;
1162                         statement = lockedbackup.substr(lockedlen, statementlen);
1163                         lockedbackup = lockedbackup.substr(0,lockedlen);
1164                         locked.innerHTML = lockedbackup;
1165                         unlocked.innerHTML = statement + unlocked.innerHTML;
1166                         metasenv = xml.getElementsByTagName("meta");
1167                         populate_goalarray(metasenv);
1168                         init_hyperlinks();
1169                         init_autotraces();
1170                         strip_anchors();
1171                         // unlocked.scrollIntoView(true);
1172                         smartScroll();
1173                 } else {
1174                         error("retract failed");
1175                 }
1176                 resume();
1177         };
1178         pause();
1179         callServer("retract",processor);
1180 }
1181
1182 function openFile()
1183 {
1184         processor = function(xml)
1185         {
1186                 if (is_defined(xml)) {
1187                         lockedbackup = "";
1188                         locked.innerHTML = lockedbackup;
1189                         unlocked.innerHTML = xml.documentElement.wholeText;
1190                         strip_anchors();
1191                 } else {
1192                         error("file open failed");
1193                 }
1194         };
1195         callServer("open",processor,"file=" + escape(filename.value));
1196 }
1197
1198 function retrieveFile(thefile)
1199 {
1200         processor = function(xml)
1201         {
1202                 if (is_defined(xml)) {
1203                    if (!is_defined(xml.getElementsByTagName("error")[0])) {
1204                         changeFile(thefile);
1205                         matita.disambMode = false;
1206                         matita.proofMode = false;
1207                         updateSide();
1208                         lockedbackup = ""
1209                         locked.innerHTML = lockedbackup;
1210                         // code originally used in google chrome (problems with mozilla)
1211                         // debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
1212                         // unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
1213                         debug(xml.childNodes[0].textContent);
1214                         if (document.all) { // IE
1215                           unlocked.innerHTML = xml.childNodes[0].text;
1216                         } else {
1217                           unlocked.innerHTML = xml.childNodes[0].textContent;
1218                         }
1219                         strip_anchors();
1220                         init_hyperlinks();
1221                         init_autotraces();
1222
1223                    } else {
1224                         error("file open failed");
1225                    }
1226                 } else {
1227                    window.location = "/login.html";
1228                 }
1229         };
1230         abortDialog("dialogBox");
1231         callServer("open",processor,"file=" + escape(thefile));
1232 }
1233
1234 function go_external_hyperlink(uri,thefile,id)
1235 {
1236         processor = function(xml)
1237         {
1238                 if (is_defined(xml)) {
1239                         // code originally used in google chrome (problems with mozilla)
1240                         // debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
1241                         // unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
1242                         // debug(xml.childNodes[0].textContent);
1243                         var doctext;
1244                         if (document.all) { // IE
1245                           doctext = xml.childNodes[0].text;
1246                         } else {
1247                           doctext= xml.childNodes[0].textContent;
1248                         }
1249                         $('#locked').html(doctext);
1250                         try {
1251                           // scroll to anchor (if it exists)
1252                           $('#' + id).scrollIntoView(true);
1253                         } catch (e) { }
1254                         init_hyperlinks();
1255                         init_autotraces();
1256                 } else {
1257                         $('#locked').html("404 object not found");
1258                 }
1259         };
1260         callServer("open",processor,"file=" + escape(thefile) + "&readonly=true");
1261 }
1262
1263 function createDocWin(uri,id) {
1264   // 12 = position of the second '/' in uri (to strip off "cic:/matita/")
1265   var thefile = uri.substring(12) + ".ma";
1266   var title = "Matita Browser - " + uri;
1267   var docWin = window.open( "", "matitabrowser",
1268      "width=800,height=600,location=no,menubar=no,status=no,scrollbars,resizable,screenX=20,screenY=40,left=20,top=40");
1269   docWin.document.write('<html><head><title>' + title + '</title>' +
1270                         '<script type="text/javascript" src="jquery.js"></script>' +
1271                         '<script type="text/javascript" src="jquery.tooltip.min.js"></script>' +
1272                         '<script type="text/javascript" src="matitaweb.js"></script>' +
1273                         '<script type="text/javascript">go_external_hyperlink("' + uri + '","' + thefile + '","' + id + '");</script>' +
1274                         '<link rel="stylesheet" type="text/css" href="matitaweb.css"/>' +
1275                         '<link rel="stylesheet" type="text/css" href="jquery.tooltip.css"/>' +
1276                         '</head>');
1277   docWin.document.write('<body><H1>'+ uri + '</H1>' +
1278                       '<pre id="locked"></pre></body></html>');
1279   docWin.document.close();
1280   docWin.baseuri = uri;
1281   return docWin;
1282 }
1283
1284 function showLibrary(title,callback,reloadDialog)
1285 {
1286         var req = null;
1287         dialogBox.reload = reloadDialog;
1288         // pause();
1289         if (window.XMLHttpRequest)
1290         {
1291                 req = new XMLHttpRequest();
1292         }
1293         else if (window.ActiveXObject)
1294         {
1295                 try {
1296                                 req = new ActiveXObject("Msxml2.XMLHTTP");
1297                 } catch (e)
1298                 {
1299                         try {
1300                                 req = new ActiveXObject("Microsoft.XMLHTTP");
1301                                 } catch (e) {}
1302                 }
1303         }
1304         req.onreadystatechange = function()
1305         {
1306
1307                 rs = req.readyState;
1308
1309                 if(rs == 4)
1310                 {
1311                         stat = req.status;
1312                         stxt = req.statusText;
1313                         if(stat == 200)
1314                         {
1315                           debug(req.responseText);
1316                           showDialog("<H2>" + title + "</H2>",req.responseText, callback);
1317                         }
1318                 }
1319         };
1320         req.open("POST", "viewlib"); // + escape(unlocked.innerHTML), true);
1321         req.setRequestHeader("Content-type","application/x-www-form-urlencoded");
1322         req.send();
1323
1324 }
1325
1326 function uploadDialog()
1327 {
1328         uploadBox.style.display = "block";
1329 }
1330
1331 function uploadOK()
1332 {
1333    var file = document.getElementById("uploadFilename").files[0];
1334 //   if (file) {
1335 //       var filecontent = file.getAsText("UTF-8");
1336 //       locked.innerHTML = lockedbackup;
1337 //       unlocked.innerHTML = filecontent;
1338 //       uploadBox.style.display = "none";
1339 //   }
1340    if (file) {
1341       var reader = new FileReader();
1342       reader.onerror = function (evt) {
1343            error("file open failed");
1344       }
1345       reader.onload = function (evt) {
1346            lockedbackup = "";
1347            locked.innerHTML = lockedbackup
1348            unlocked.innerHTML = "";
1349            unlocked.appendChild(document.createTextNode(evt.target.result));
1350            uploadBox.style.display = "none";
1351       }
1352       try { reader.readAsText(file, "UTF-8"); }
1353       catch (err) { /* nothing to do */ };
1354       uploadBox.style.display = "none";
1355    }
1356 }
1357
1358 function openDialog()
1359 {
1360         callback = function (fname) { retrieveFile(fname); };
1361         showLibrary("Open file", callback, openDialog);
1362 }
1363
1364 function saveDialog()
1365 {
1366         callback = function (fname) {
1367           abortDialog("dialogBox");
1368           saveFile(fname,
1369                    (locked.innerHTML.html_to_matita()).sescape(),
1370                    (unlocked.innerHTML.html_to_matita()).sescape(),
1371                    false,saveDialog);
1372         };
1373         showLibrary("Save file as", callback, saveDialog);
1374 }
1375
1376 function newDialog()
1377 {
1378         callback = function (fname) {
1379           abortDialog("dialogBox");
1380           saveFile(fname,"","",false,newDialog,true);
1381         };
1382         showLibrary("Create new file", callback, newDialog);
1383 }
1384
1385
1386 function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog,reloadFile)
1387 {
1388         if (!is_defined(reloadFile)) { reloadFile = true };
1389         if (!is_defined(fname)) {
1390             fname = current_fname;
1391             lockedtxt = (locked.innerHTML.html_to_matita()).sescape();
1392             unlockedtxt = (unlocked.innerHTML.html_to_matita()).sescape();
1393             force = true;
1394             // when force is true, reloadDialog is not needed
1395         }
1396         processor = function(xml) {
1397                 if (is_defined(xml)) {
1398                   if (xml.childNodes[0].textContent != "ok") {
1399                     if (confirm("File already exists. All existing data will be lost.\nDo you want to proceed anyway?")) {
1400                        saveFile(fname,lockedtxt,unlockedtxt,true,reloadDialog,reloadFile);
1401                     } else {
1402                       reloadDialog();
1403                     }
1404                   } else {
1405                     changeFile(fname);
1406                     debug("file saved!");
1407                     if (reloadFile) { retrieveFile(fname); }
1408                   }
1409                 } else {
1410                         error("save file failed");
1411                 }
1412                 resume();
1413         };
1414         if (is_defined(fname)) {
1415           pause();
1416           callServer("save",processor,"file=" + escape(fname) +
1417                                     "&locked=" + lockedtxt +
1418                                     "&unlocked=" + unlockedtxt +
1419                                     "&force=" + force);
1420         }
1421         else { error("no file selected"); }
1422 }
1423
1424 function createDir() {
1425    abortDialog("dialogBox");
1426    dirname = prompt("New directory name:\ncic:/matita/","newdir");
1427    if (dirname != null) {
1428         processor = function(xml) {
1429                 if (is_defined(xml)) {
1430                   if (xml.childNodes[0].textContent != "ok") {
1431                       alert("An error occurred :-(");
1432                   }
1433                 } else {
1434                       alert("An error occurred :-(");
1435                 }
1436                 dialogBox.reload();
1437         };
1438         pause();
1439         callServer("save",processor,"file=" + escape(dirname) +
1440                                     "&locked=&unlocked=&force=false&dir=true");
1441    } else {
1442       dialogBox.reload();
1443    }
1444 }
1445
1446 function commitAll()
1447 {
1448         processor = function(xml) {
1449                 if (is_defined(xml)) {
1450                         debug(xml.getElementsByTagName("details")[0].textContent);
1451                         alert("Commit executed: see details in the log.\n\n" +
1452                               "NOTICE: this message does NOT imply (yet) that the commit was successful.");
1453                 } else {
1454                         alert("Commit failed!");
1455                 }
1456                 resume();
1457         };
1458         pause();
1459         callServer("commit",processor);
1460 }
1461
1462 function updateAll()
1463 {
1464         processor = function(xml) {
1465                 if (is_defined(xml)) {
1466                         alert("Update executed.\n\n" +
1467                               "Details:\n" +
1468                               xml.getElementsByTagName("details")[0].textContent);
1469                 } else {
1470                         alert("Update failed!");
1471                 }
1472                 resume();
1473         };
1474         pause();
1475         callServer("update",processor);
1476 }
1477
1478 var goalcell;
1479
1480 function hideSequent() {
1481         matita.proofMode = false;
1482         updateSide();
1483 }
1484
1485 function showSequent() {
1486         matita.proofMode = true;
1487         updateSide();
1488 }
1489
1490 function showDialog(title,content,callback) {
1491   dialogTitle.innerHTML = title;
1492   dialogContent.innerHTML = content;
1493   dialogBox.callback = callback;
1494
1495   //Get the screen height and width
1496   var maskHeight = $(document).height();
1497   var maskWidth = $(window).width();
1498
1499   //Set heigth and width to mask to fill up the whole screen
1500   $('#mask').css({'width':maskWidth,'height':maskHeight});
1501
1502   //transition effect
1503   $('#mask').fadeIn(100);
1504   $('#mask').fadeTo(200,0.8);
1505
1506   //Get the window height and width
1507   var winH = $(window).height();
1508   var winW = $(window).width();
1509
1510   //Set the popup window to center
1511   $('#dialogBox').css('top',  winH/2-$('#dialogBox').height()/2);
1512   $('#dialogBox').css('left', winW/2-$('#dialogBox').width()/2);
1513
1514   //transition effect
1515   $('#dialogBox').fadeIn(200);
1516
1517   dialogBox.style.display = "block";
1518 }
1519
1520 function abortDialog(dialog) {
1521   document.getElementById(dialog).style.display = "none";
1522   $('#mask').hide();
1523 }
1524
1525 function removeElement(id) {
1526   var element = document.getElementById(id);
1527   element.parentNode.removeChild(element);
1528 }
1529
1530 var savedsc;
1531 var savedso;
1532
1533 function getCursorPos() {
1534   var cursorPos;
1535   if (window.getSelection) {
1536     var selObj = window.getSelection();
1537     savedRange = selObj.getRangeAt(0);
1538     savedsc = savedRange.startContainer;
1539     savedso = savedRange.startOffset;
1540     //cursorPos =  findNode(selObj.anchorNode.parentNode.childNodes, selObj.anchorNode) + selObj.anchorOffset;
1541     cursorPos =  findNode(unlocked.childNodes, selObj.anchorNode,0) + selObj.anchorOffset;
1542     /* FIXME the following works wrong in Opera when the document is longer than 32767 chars */
1543     return(cursorPos);
1544   }
1545   else if (document.selection) {
1546     savedRange = document.selection.createRange();
1547     var bookmark = savedRange.getBookmark();
1548     /* FIXME the following works wrong when the document is longer than 65535 chars */
1549     cursorPos = bookmark.charCodeAt(2) - 11; /* Undocumented function [3] */
1550     return(cursorPos);
1551   }
1552 }
1553
1554 function findNode(list, node, acc) {
1555   for (var i = 0; i < list.length; i++) {
1556     if (list[i] == node) {
1557    //   debug("success " + i);
1558       return acc;
1559     }
1560     if (list[i].hasChildNodes()) {
1561        try {
1562    //      debug("recursion on node " + i);
1563          return (findNode(list[i].childNodes,node,acc))
1564        }
1565        catch (e) { /* debug("recursion failed"); */ }
1566     }
1567     sandbox = document.getElementById("sandbox");
1568     dup = list[i].cloneNode(true);
1569     sandbox.appendChild(dup);
1570 //    debug("fail " + i + ": " + sandbox.innerHTML);
1571     acc += sandbox.innerHTML.html_to_matita().length;
1572     sandbox.removeChild(dup);
1573   }
1574   throw "not found";
1575 }
1576
1577 function test () {
1578   debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos()));
1579 }
1580
1581 function get_checked_index(name) {
1582         var radios = document.getElementsByName(name);
1583         for (i = 0; i < radios.length; i++) {
1584             if (radios[i].checked) {
1585                     return i;
1586             }
1587         }
1588         return null;
1589 }
1590
1591 function cancel_disambiguate() {
1592         matita.disambMode = false;
1593         resume();
1594         // enable_toparea();
1595         // enable_editing();
1596         strip_tags("span","error");
1597         updateSide();
1598 }
1599
1600 function do_disambiguate() {
1601         var i = get_checked_index("interpr");
1602         if (i != null) {
1603             var pre = matita.unlockedbackup
1604                       .substring(0,matita.ambiguityStart).matita_to_html();
1605             var mid = matita.unlockedbackup
1606                       .substring(matita.ambiguityStart,matita.ambiguityStop)
1607                       .matita_to_html();
1608             var post = matita.unlockedbackup
1609                        .substring(matita.ambiguityStop).matita_to_html();
1610
1611             var href = matita.interpretations[i].href;
1612             var title = matita.interpretations[i].title;
1613
1614             if (is_defined(title)) {
1615                 mid = "<A href=\"" + href + "\" title=\"" + title + "\">" + mid + "</A>";
1616             } else {
1617                 mid = "<A href=\"" + href + "\">" + mid + "</A>";
1618             }
1619
1620             unlocked.innerHTML = pre + mid + post;
1621
1622             matita.disambMode = false;
1623             enable_toparea();
1624             enable_editing();
1625             updateSide();
1626         }
1627 }
1628
1629 function do_showerror() {
1630         var i = get_checked_index("choice");
1631         if (i != null) {
1632             var pre = matita.unlockedbackup
1633                       .substring(0,matita.ambiguityStart).matita_to_html();
1634             var mid = matita.unlockedbackup
1635                       .substring(matita.ambiguityStart,matita.ambiguityStop)
1636                       .matita_to_html();
1637             var post = matita.unlockedbackup
1638                        .substring(matita.ambiguityStop).matita_to_html();
1639
1640             var href = matita.interpretations[i].href;
1641             var title = matita.interpretations[i].title;
1642
1643             if (is_defined(title)) {
1644                 mid = "<A href=\"" + href + "\" title=\"" + title + "\">" + mid + "</A>";
1645             } else {
1646                 mid = "<A href=\"" + href + "\">" + mid + "</A>";
1647             }
1648
1649             unlocked.innerHTML = pre + mid + post;
1650
1651         }
1652 }
1653
1654 function readCookie(name) {
1655         var nameEQ = name + "=";
1656         var ca = document.cookie.split(';');
1657         for(var i=0;i < ca.length;i++) {
1658                 var c = ca[i];
1659                 while (c.charAt(0)==' ') c = c.substring(1,c.length);
1660                 if (c.indexOf(nameEQ) == 0) return c.substring(nameEQ.length,c.length);
1661         }
1662         return null;
1663 }
1664
1665 function delete_cookie ( cookie_name )
1666 {
1667   var cookie_date = new Date();  // current date & time
1668   cookie_date.setTime ( cookie_date.getTime() - 1 );
1669   document.cookie = cookie_name += "=; expires=" + cookie_date.toGMTString();
1670 }
1671
1672 function delete_session()
1673 {
1674         delete_cookie("session");
1675 }
1676
1677 function disable_toparea() {
1678         var offset = $('#toparea').offset();
1679         $('#whitemask').css('top',offset.top);
1680         $('#whitemask').css('left',offset.left);
1681         $('#whitemask').css('width',$('#toparea').outerWidth() + "px");
1682         $('#whitemask').css('height',$('#toparea').outerHeight() + "px");
1683         $('#whitemask').fadeTo('fast',0.7);
1684 }
1685
1686 function enable_toparea() {
1687         $('#whitemask').hide();
1688 }
1689
1690 function disable_editing() {
1691         unlocked.contentEditable = false;
1692 }
1693
1694 function enable_editing() {
1695         unlocked.contentEditable = true;
1696 }
1697
1698 function pause()
1699 {
1700         // advanceButton.disabled = true;
1701         // retractButton.disabled = true;
1702         // cursorButton.disabled = true;
1703         // bottomButton.disabled = true;
1704         disable_toparea();
1705         disable_editing();
1706 }
1707
1708 function resume()
1709 {
1710         // advanceButton.disabled = false;
1711         // retractButton.disabled = false;
1712         // cursorButton.disabled = false;
1713         // bottomButton.disabled = false;
1714         if (!matita.disambMode) {
1715                 enable_toparea();
1716                 enable_editing();
1717         }
1718 }
1719
1720 function test()
1721 {
1722         xx.onclick();
1723 }