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 = "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 = $("#unlocked " + tagname + "." + classname);
 266     } else {
 267       tags = $("#unlocked " + 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("IMG","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         var localized = xml.getElementsByTagName("localized")[0];
 656         if (is_defined(parsed)) {
 657         // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
 658             var len = parseInt(parsed.getAttribute("length"));
 659             if (len > 0) {
 660               // len0 = unlocked.innerHTML.length;
 661               var unescaped = unlocked.innerHTML.html_to_matita();
 662               var parsedtxt = parsed.childNodes[0].wholeText;
 663               //parsedtxt = unescaped.substr(0,len);
 664               var unparsedtxt = unescaped.substr(len);
 665               lockedbackup += parsedtxt;
 666               locked.innerHTML = lockedbackup;
 667               unlocked.innerHTML = unparsedtxt.matita_to_html();
 668               // len1 = unlocked.innerHTML.length;
 669               // len2 = len0 - len1;
 670               var len2 = parsedtxt.length;
 671               metasenv = xml.getElementsByTagName("meta");
 672               statements = listcons(len2,statements);
 673               //unlocked.scrollIntoView(true);
 674               smartScroll();
 675             }
 676             return len;
 677         }
 678         else if (is_defined(ambiguity)) {
 679             var start = parseInt(ambiguity.getAttribute("start"));
 680             var stop = parseInt(ambiguity.getAttribute("stop"));
 681             var choices = xml.getElementsByTagName("choice");
 682
 683             matita.ambiguityStart = start;
 684             matita.ambiguityStop = stop;
 685             matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
 686             matita.interpretations = [];
 687
 688             var unlockedtxt = unlocked.innerHTML.html_to_matita();
 689             var pre = unlockedtxt.substring(0,start).matita_to_html();
 690             var mid = unlockedtxt.substring(start,stop).matita_to_html();
 691             var post = unlockedtxt.substring(stop).matita_to_html();
 692             unlocked.innerHTML = pre +
 693                     "<span class=\"error\" title=\"disambiguation error\">" +
 694                     mid + "</span>" + post;
 695
 696             var title = "<H3>Ambiguous input</H3>";
 697             disambcell.innerHTML = title;
 698             for (i = 0;i < choices.length;i++) {
 699                 matita.interpretations[i] = new Object();
 700
 701                 var href = choices[i].getAttribute("href");
 702                 var title = choices[i].getAttribute("title");
 703                 var desc = choices[i].childNodes[0].nodeValue;
 704
 705                 matita.interpretations[i].href = href;
 706                 matita.interpretations[i].title = title;
 707                 matita.interpretations[i].desc = desc;
 708
 709                 var choice = document.createElement("input");
 710                 choice.setAttribute("type","radio");
 711                 choice.setAttribute("name","interpr");
 712                 choice.setAttribute("href",href);
 713                 choice.setAttribute("title",title);
 714                 if (i == 0) choice.setAttribute("checked","");
 715
 716                 disambcell.appendChild(choice);
 717                 disambcell.appendChild(document.createTextNode(desc));
 718                 disambcell.appendChild(document.createElement("br"));
 719             }
 720
 721             var okbutton = document.createElement("input");
 722             okbutton.setAttribute("type","button");
 723             okbutton.setAttribute("value","OK");
 724             okbutton.setAttribute("onclick","do_disambiguate()");
 725             var cancelbutton = document.createElement("input");
 726             cancelbutton.setAttribute("type","button");
 727             cancelbutton.setAttribute("value","Cancel");
 728             cancelbutton.setAttribute("onclick","cancel_disambiguate()");
 729
 730             disambcell.appendChild(okbutton);
 731             disambcell.appendChild(cancelbutton);
 732
 733             matita.disambMode = true;
 734             updateSide();
 735             throw "Stop";
 736         }
 737         else if (is_defined(disamberr)) {
 738             // must be fixed in a daemon: it makes sense to return a
 739             // disambiguation error with no choices
 740             if (disamberr.childNodes.length > 0) {
 741               set_cps(disamberr.childNodes);
 742               matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
 743               matita.disambMode = true;
 744               next_cp(0);
 745             }
 746             throw "Stop";
 747         } else if (is_defined(localized)) {
 748             unlocked.innerHTML = localized.childNodes[0].wholeText;
 749             throw "Stop";
 750         }
 751         else {
 752             var err = xml.getElementsByTagName("error")[0];
 753             error(err.childNodes[0].nodeValue);
 754             throw "Stop";
 755         }
 756
 757 }
 758
 759 function advanceForm1()
 760 {
 761         processor = function(xml) {
 762            try {
 763                 if (is_defined(xml)) {
 764                     advOneStep(xml);
 765                     populate_goalarray(metasenv);
 766                     init_hyperlinks();
 767                     init_autotraces();
 768                 } else {
 769                         error("advance failed");
 770                 }
 771             } catch (e) {
 772                     // nothing to do
 773             };
 774             resume();
 775         };
 776         pause();
 777         callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
 778
 779 }
 780
 781 // get or set <choicepoint>'s (in case of disamb error)
 782 function get_cps() {
 783         return matita.choicepoints
 784 }
 785
 786 function set_cps(cps) {
 787         matita.choicepoints = cps;
 788 }
 789
 790 // get radio buttons for <choice>'s in a given cp
 791 function get_choice_opts(i) {
 792    var res = [];
 793    var choices = get_cps()[i].childNodes;
 794    for (var j = 0;j < choices.length;j++) {
 795       var href = choices[j].getAttribute("href");
 796       var title = choices[j].getAttribute("title");
 797       var desc;
 798       if (is_defined(title) && title != null) {
 799            desc = title;
 800       } else if (is_defined(href) && href != null) {
 801            desc = href;
 802       } else {
 803            desc = null;
 804       }
 805
 806       res[j] = document.createElement("input");
 807       res[j].setAttribute("type","radio");
 808       res[j].setAttribute("name","choice");
 809       res[j].setAttribute("choicepointno",i);
 810       res[j].setAttribute("choiceno",j);
 811       res[j].setAttribute("href",href);
 812       res[j].setAttribute("title",title);
 813       if (desc != null) res[j].setAttribute("desc",desc);
 814
 815       if (j == 0) res[j].setAttribute("checked","");
 816   }
 817   return res;
 818 }
 819
 820 // get radio buttons for <failure>'s in a given choice
 821 function get_failure_opts(i,j) {
 822    var res = [];
 823    var failures = get_cps()[i].childNodes[j].childNodes;
 824    for (var k = 0;k < failures.length;k++) {
 825       var start = failures[k].getAttribute("start");
 826       var stop = failures[k].getAttribute("stop");
 827       var title = failures[k].getAttribute("title");
 828
 829       res[k] = document.createElement("input");
 830       res[k].setAttribute("type","radio");
 831       res[k].setAttribute("name","failure");
 832       res[k].setAttribute("choicepointno",i);
 833       res[k].setAttribute("choiceno",j);
 834       res[k].setAttribute("failureno",k);
 835       res[k].setAttribute("start",start);
 836       res[k].setAttribute("stop",stop);
 837       res[k].setAttribute("title",title);
 838
 839       if (k == 0) res[k].setAttribute("checked","");
 840   }
 841   return res;
 842 }
 843
 844 function next_cp(curcp) {
 845         var cp = get_cps()[curcp];
 846         var start = parseInt(cp.getAttribute("start"));
 847         var stop = parseInt(cp.getAttribute("stop"));
 848
 849         matita.errorStart = start;
 850         matita.errorStop = stop;
 851         // matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
 852
 853         var unlockedtxt = matita.unlockedbackup;
 854         var pre = unlockedtxt.substring(0,start).matita_to_html();
 855         var mid = unlockedtxt.substring(start,stop).matita_to_html();
 856         var post = unlockedtxt.substring(stop).matita_to_html();
 857         unlocked.innerHTML = pre +
 858                 "<span class=\"error\" title=\"error location\">" +
 859                 mid + "</span>" + post;
 860
 861         var title = "<H3>Error diagnostics</H3>";
 862         disambcell.innerHTML = title;
 863         var choices = get_choice_opts(curcp);
 864         for (var i = 0;i < choices.length;i++) {
 865             disambcell.appendChild(choices[i]);
 866             var desc = choices[i].getAttribute("desc");
 867             if (!is_defined(desc) || desc == null) {
 868                     desc = "Interpretation " + i;
 869             }
 870             disambcell.appendChild(document.createTextNode(desc));
 871             disambcell.appendChild(document.createElement("br"));
 872         }
 873
 874         // update index of the next choicepoint
 875         new_curcp = (curcp + 1) % get_cps().length;
 876
 877         var okbutton = document.createElement("input");
 878         okbutton.setAttribute("type","button");
 879         okbutton.setAttribute("value","OK");
 880         okbutton.setAttribute("onclick","show_failures()");
 881         var cancelbutton = document.createElement("input");
 882         cancelbutton.setAttribute("type","button");
 883         cancelbutton.setAttribute("value","Close");
 884         cancelbutton.setAttribute("onclick","cancel_disambiguate()");
 885         var tryagainbutton = document.createElement("input");
 886         tryagainbutton.setAttribute("type","button");
 887         if (new_curcp > 0) {
 888             tryagainbutton.setAttribute("value","Try something else");
 889         } else {
 890             tryagainbutton.setAttribute("value","Restart");
 891         }
 892         tryagainbutton.setAttribute("onclick","next_cp(" + new_curcp + ")");
 893
 894         disambcell.appendChild(okbutton);
 895         disambcell.appendChild(tryagainbutton);
 896         disambcell.appendChild(cancelbutton);
 897
 898         //disable_toparea();
 899
 900         //matita.disambMode = true;
 901         updateSide();
 902
 903 }
 904
 905 function show_failures() {
 906
 907         var choice = document.getElementsByName("choice")[get_checked_index("choice")];
 908         var cpno = parseInt(choice.getAttribute("choicepointno"));
 909         var choiceno = parseInt(choice.getAttribute("choiceno"));
 910         var choicedesc = choice.getAttribute("desc");
 911
 912         var title = "<H3>Error diagnostics</H3>";
 913         var subtitle;
 914         if (is_defined(choicedesc) && choicedesc != null) {
 915                 subtitle  = "<p>Errors at node " + cpno + " = " + choicedesc + "</p>";
 916         } else {
 917                 subtitle = "<p>Global errors:</p>";
 918         }
 919
 920         disambcell.innerHTML = title + subtitle;
 921         var failures = get_failure_opts(cpno,choiceno);
 922         for (var i = 0;i < failures.length;i++) {
 923             disambcell.appendChild(failures[i]);
 924             disambcell.appendChild(document.createTextNode(failures[i].getAttribute("title")));
 925             disambcell.appendChild(document.createElement("br"));
 926         }
 927
 928         var okbutton = document.createElement("input");
 929         okbutton.setAttribute("type","button");
 930         okbutton.setAttribute("value","Show error loc");
 931         okbutton.setAttribute("onclick","show_err()");
 932         var cancelbutton = document.createElement("input");
 933         cancelbutton.setAttribute("type","button");
 934         cancelbutton.setAttribute("value","Close");
 935         cancelbutton.setAttribute("onclick","cancel_disambiguate()");
 936         var backbutton = document.createElement("input");
 937         backbutton.setAttribute("type","button");
 938         backbutton.setAttribute("value","<< Back");
 939         backbutton.setAttribute("onclick","next_cp(" + cpno + ")");
 940
 941         disambcell.appendChild(backbutton);
 942         disambcell.appendChild(okbutton);
 943         disambcell.appendChild(cancelbutton);
 944
 945 }
 946
 947 function show_err() {
 948         var radios = document.getElementsByName("failure");
 949         for (i = 0; i < radios.length; i++) {
 950             if (radios[i].checked) {
 951                 var start = radios[i].getAttribute("start");
 952                 var stop = radios[i].getAttribute("stop");
 953                 var title = radios[i].getAttribute("title");
 954                 var unlockedtxt = matita.unlockedbackup;
 955                 var pre = unlockedtxt.substring(0,start).matita_to_html();
 956                 var mid = unlockedtxt.substring(start,stop).matita_to_html();
 957                 var post = unlockedtxt.substring(stop).matita_to_html();
 958                 unlocked.innerHTML = pre +
 959                         "<span class=\"error\" title=\"Disambiguation failure\">" +
 960                         mid + "</span>" + post;
 961                 break;
 962             }
 963         }
 964 }
 965
 966 function gotoBottom()
 967 {
 968         processor = function(xml) {
 969                 if (is_defined(xml)) {
 970                         // debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND");
 971                         var parsed = xml.getElementsByTagName("parsed");
 972                         var localized = xml.getElementsByTagName("localized")[0];
 973                         var ambiguity = xml.getElementsByTagName("ambiguity")[0];
 974                         var generic_err = xml.getElementsByTagName("error")[0];
 975                         var disamberr = xml.getElementsByTagName("disamberror")[0];
 976                         for (var i = 0;i < parsed.length; i++) {
 977                           var len = parsed[i].getAttribute("length");
 978                           // len0 = unlocked.innerHTML.length;
 979                           var unescaped = unlocked.innerHTML.html_to_matita();
 980                           // the browser may decide to split textnodes: use wholeText!
 981                           var parsedtxt = parsed[i].childNodes[0].wholeText;
 982                           //parsedtxt = unescaped.substr(0,len);
 983                           var unparsedtxt = unescaped.substr(len);
 984                           lockedbackup += parsedtxt;
 985                           locked.innerHTML = lockedbackup; //.matita_to_html();
 986                           unlocked.innerHTML = unparsedtxt.matita_to_html();
 987                           // len1 = unlocked.innerHTML.length;
 988                           var len2 = parsedtxt.length;
 989                           statements = listcons(len2,statements);
 990                         }
 991                         // unlocked.scrollIntoView(true);
 992                         smartScroll();
 993                         metasenv = xml.getElementsByTagName("meta");
 994                         init_hyperlinks();
 995                         init_autotraces();
 996                         populate_goalarray(metasenv);
 997
 998                         if (is_defined(ambiguity)) {
 999                             var start = parseInt(ambiguity.getAttribute("start"));
1000                             var stop = parseInt(ambiguity.getAttribute("stop"));
1001                             var choices = xml.getElementsByTagName("choice");
1002
1003                             matita.ambiguityStart = start;
1004                             matita.ambiguityStop = stop;
1005                             matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
1006                             matita.interpretations = [];
1007
1008                             var unlockedtxt = unlocked.innerHTML.html_to_matita();
1009                             var pre = unlockedtxt.substring(0,start).matita_to_html();
1010                             var mid = unlockedtxt.substring(start,stop).matita_to_html();
1011                             var post = unlockedtxt.substring(stop).matita_to_html();
1012                             unlocked.innerHTML = pre +
1013                                     "<span class=\"error\" title=\"disambiguation error\">" +
1014                                     mid + "</span>" + post;
1015
1016                             var title = "<H3>Ambiguous input</H3>";
1017                             disambcell.innerHTML = title;
1018                             for (i = 0;i < choices.length;i++) {
1019                                 matita.interpretations[i] = new Object();
1020
1021                                 var href = choices[i].getAttribute("href");
1022                                 var title = choices[i].getAttribute("title");
1023                                 var desc = choices[i].childNodes[0].nodeValue;
1024
1025                                 matita.interpretations[i].href = href;
1026                                 matita.interpretations[i].title = title;
1027                                 matita.interpretations[i].desc = desc;
1028
1029                                 var choice = document.createElement("input");
1030                                 choice.setAttribute("type","radio");
1031                                 choice.setAttribute("name","interpr");
1032                                 choice.setAttribute("href",href);
1033                                 choice.setAttribute("title",title);
1034                                 if (i == 0) choice.setAttribute("checked","");
1035
1036                                 disambcell.appendChild(choice);
1037                                 disambcell.appendChild(document.createTextNode(desc));
1038                                 disambcell.appendChild(document.createElement("br"));
1039                             }
1040
1041                             var okbutton = document.createElement("input");
1042                             okbutton.setAttribute("type","button");
1043                             okbutton.setAttribute("value","OK");
1044                             okbutton.setAttribute("onclick","do_disambiguate()");
1045                             var cancelbutton = document.createElement("input");
1046                             cancelbutton.setAttribute("type","button");
1047                             cancelbutton.setAttribute("value","Cancel");
1048                             cancelbutton.setAttribute("onclick","cancel_disambiguate()");
1049
1050                             disambcell.appendChild(okbutton);
1051                             disambcell.appendChild(cancelbutton);
1052
1053                             matita.disambMode = true;
1054                             updateSide();
1055                         }
1056                         else if (is_defined(disamberr)) {
1057                             // must be fixed in a daemon: it makes sense to return a
1058                             // disambiguation error with no choices
1059                             if (disamberr.childNodes.length > 0) {
1060                               set_cps(disamberr.childNodes);
1061                               matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
1062                               matita.disambMode = true;
1063                               next_cp(0);
1064                             }
1065                             throw "Stop";
1066                         }
1067                         else if (is_defined(localized)) {
1068                             unlocked.innerHTML = localized.childNodes[0].wholeText;
1069                         }
1070                         else if (is_defined(generic_err)) {
1071                             error("Unmanaged error:\n" + generic_err.childNodes[0].wholeText);
1072                         }
1073                 } else {
1074                         error("goto bottom failed");
1075                 }
1076                 resume();
1077         };
1078         pause();
1079         callServer("bottom",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
1080 }
1081
1082
1083 function gotoTop()
1084 {
1085         processor = function(xml) {
1086                 if (is_defined(xml)) {
1087                   if (xml.childNodes[0].textContent != "ok") {
1088                      error("goto top failed");
1089                   }
1090                   else
1091                         statements = listnil();
1092                         /*
1093                         lockedlen = locked.innerHTML.length - statementlen;
1094                         statement = locked.innerHTML.substr(lockedlen, statementlen);
1095                         locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
1096                         unlocked.innerHTML = statement + unlocked.innerHTML;
1097                         */
1098                         unlocked.innerHTML = lockedbackup + unlocked.innerHTML;
1099                         lockedbackup = "";
1100                         locked.innerHTML = lockedbackup;
1101                         init_hyperlinks();
1102                         init_autotraces();
1103                         hideSequent();
1104                         strip_anchors();
1105                         // unlocked.scrollIntoView(true);
1106                         smartScroll();
1107                 } else {
1108                         error("goto top failed");
1109                 }
1110                 resume();
1111         };
1112         pause();
1113         callServer("top",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
1114
1115 }
1116
1117 function gotoPos(offset)
1118 {
1119         if (!is_defined(offset)) {
1120                 offset = getCursorPos();
1121         }
1122         processor = function(xml) {
1123                 if (is_defined(xml)) {
1124                     try {
1125                         var len = advOneStep(xml);
1126                         if (len == 0 || offset <= len) {
1127                                 init_hyperlinks();
1128                                 init_autotraces();
1129                                 populate_goalarray(metasenv);
1130                                 resume();
1131                         } else {
1132                                 gotoPos(offset - len);
1133                         }
1134                     } catch (er) {
1135                         init_hyperlinks();
1136                         init_autotraces();
1137                         populate_goalarray(metasenv);
1138                         resume();
1139                     }
1140                 } else {
1141                         init_hyperlinks();
1142                         init_autotraces();
1143                         // unlocked.scrollIntoView(true);
1144                         smartScroll();
1145                         populate_goalarray(metasenv);
1146                         resume();
1147                 }
1148         }
1149         pause();
1150         callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
1151 }
1152
1153 function retractStep()
1154 {
1155     if (!is_nil(statements)) {
1156         processor = function(xml) {
1157                 if (typeof xml != "undefined") {
1158                         // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
1159                         statementlen = parseInt(listhd(statements));
1160                         statements = listtl(statements);
1161                         /*
1162                         lockedlen = locked.innerHTML.length - statementlen;
1163                         statement = locked.innerHTML.substr(lockedlen, statementlen);
1164                         locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
1165                         unlocked.innerHTML = statement + unlocked.innerHTML;
1166                         */
1167                         lockedlen = lockedbackup.length - statementlen;
1168                         statement = lockedbackup.substr(lockedlen, statementlen);
1169                         lockedbackup = lockedbackup.substr(0,lockedlen);
1170                         locked.innerHTML = lockedbackup;
1171                         unlocked.innerHTML = statement + unlocked.innerHTML;
1172                         metasenv = xml.getElementsByTagName("meta");
1173                         populate_goalarray(metasenv);
1174                         init_hyperlinks();
1175                         init_autotraces();
1176                         strip_anchors();
1177                         // unlocked.scrollIntoView(true);
1178                         smartScroll();
1179                 } else {
1180                         error("retract failed");
1181                 }
1182                 resume();
1183         };
1184         pause();
1185         callServer("retract",processor);
1186     }
1187 }
1188
1189 function openFile()
1190 {
1191         processor = function(xml)
1192         {
1193                 if (is_defined(xml)) {
1194                         lockedbackup = "";
1195                         locked.innerHTML = lockedbackup;
1196                         unlocked.innerHTML = xml.documentElement.wholeText;
1197                         strip_anchors();
1198                 } else {
1199                         error("file open failed");
1200                 }
1201         };
1202         callServer("open",processor,"file=" + escape(filename.value));
1203 }
1204
1205 function retrieveFile(thefile)
1206 {
1207         processor = function(xml)
1208         {
1209                 if (is_defined(xml)) {
1210                    if (!is_defined(xml.getElementsByTagName("error")[0])) {
1211                         changeFile(thefile);
1212                         matita.disambMode = false;
1213                         matita.proofMode = false;
1214                         updateSide();
1215                         lockedbackup = ""
1216                         locked.innerHTML = lockedbackup;
1217                         // code originally used in google chrome (problems with mozilla)
1218                         // debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
1219                         // unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
1220                         debug(xml.childNodes[0].textContent);
1221                         if (document.all) { // IE
1222                           unlocked.innerHTML = xml.childNodes[0].text;
1223                         } else {
1224                           unlocked.innerHTML = xml.childNodes[0].textContent;
1225                         }
1226                         strip_anchors();
1227                         init_hyperlinks();
1228                         init_autotraces();
1229                         unlocked.scrollIntoView(true);
1230                    } else {
1231                         error("file open failed");
1232                    }
1233                 } else {
1234                    window.location = "/login.html";
1235                 }
1236         };
1237         abortDialog("dialogBox");
1238         callServer("open",processor,"file=" + escape(thefile));
1239 }
1240
1241 function go_external_hyperlink(uri,thefile,id)
1242 {
1243         processor = function(xml)
1244         {
1245                 if (is_defined(xml)) {
1246                         // code originally used in google chrome (problems with mozilla)
1247                         // debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
1248                         // unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
1249                         // debug(xml.childNodes[0].textContent);
1250                         var doctext;
1251                         if (document.all) { // IE
1252                           doctext = xml.childNodes[0].text;
1253                         } else {
1254                           doctext= xml.childNodes[0].textContent;
1255                         }
1256                         $('#locked').html(doctext);
1257                         try {
1258                           // scroll to anchor (if it exists)
1259                           $('#' + id).get(0).scrollIntoView(true);
1260                         } catch (e) { }
1261                         init_hyperlinks();
1262                         init_autotraces();
1263                 } else {
1264                         $('#locked').html("404 object not found");
1265                 }
1266         };
1267         callServer("open",processor,"file=" + escape(thefile) + "&readonly=true");
1268 }
1269
1270 function createDocWin(uri,id) {
1271   // 12 = position of the second '/' in uri (to strip off "cic:/matita/")
1272   var thefile = uri.substring(12) + ".ma";
1273   var title = "Matita Browser - " + uri;
1274   var docWin = window.open( "", "matitabrowser",
1275      "width=800,height=600,location=no,menubar=no,status=no,scrollbars,resizable,screenX=20,screenY=40,left=20,top=40");
1276   docWin.document.write('<html><head><title>' + title + '</title>' +
1277                         '<script type="text/javascript" src="jquery.js"></script>' +
1278                         '<script type="text/javascript" src="jquery.tooltip.min.js"></script>' +
1279                         '<script type="text/javascript" src="matitaweb.js"></script>' +
1280                         '<script type="text/javascript">go_external_hyperlink("' + uri + '","' + thefile + '","' + id + '");</script>' +
1281                         '<link rel="stylesheet" type="text/css" href="matitaweb.css"/>' +
1282                         '<link rel="stylesheet" type="text/css" href="jquery.tooltip.css"/>' +
1283                         '</head>');
1284   docWin.document.write('<body><H1>'+ uri + '</H1>' +
1285                       '<pre id="locked"></pre></body></html>');
1286   docWin.document.close();
1287   docWin.baseuri = uri;
1288   return docWin;
1289 }
1290
1291 function showLibrary(title,callback,reloadDialog)
1292 {
1293         var req = null;
1294         dialogBox.reload = reloadDialog;
1295         // pause();
1296         if (window.XMLHttpRequest)
1297         {
1298                 req = new XMLHttpRequest();
1299         }
1300         else if (window.ActiveXObject)
1301         {
1302                 try {
1303                                 req = new ActiveXObject("Msxml2.XMLHTTP");
1304                 } catch (e)
1305                 {
1306                         try {
1307                                 req = new ActiveXObject("Microsoft.XMLHTTP");
1308                                 } catch (e) {}
1309                 }
1310         }
1311         req.onreadystatechange = function()
1312         {
1313
1314                 rs = req.readyState;
1315
1316                 if(rs == 4)
1317                 {
1318                         stat = req.status;
1319                         stxt = req.statusText;
1320                         if(stat == 200)
1321                         {
1322                           debug(req.responseText);
1323                           showDialog("<H2>" + title + "</H2>",req.responseText, callback);
1324                         }
1325                 }
1326         };
1327         req.open("POST", "viewlib"); // + escape(unlocked.innerHTML), true);
1328         req.setRequestHeader("Content-type","application/x-www-form-urlencoded");
1329         req.send();
1330
1331 }
1332
1333 function uploadDialog()
1334 {
1335         uploadBox.style.display = "block";
1336 }
1337
1338 function uploadOK()
1339 {
1340    var file = document.getElementById("uploadFilename").files[0];
1341 //   if (file) {
1342 //       var filecontent = file.getAsText("UTF-8");
1343 //       locked.innerHTML = lockedbackup;
1344 //       unlocked.innerHTML = filecontent;
1345 //       uploadBox.style.display = "none";
1346 //   }
1347    if (file) {
1348       var reader = new FileReader();
1349       reader.onerror = function (evt) {
1350            error("file open failed");
1351       }
1352       reader.onload = function (evt) {
1353            lockedbackup = "";
1354            locked.innerHTML = lockedbackup
1355            unlocked.innerHTML = "";
1356            unlocked.appendChild(document.createTextNode(evt.target.result));
1357            uploadBox.style.display = "none";
1358       }
1359       try { reader.readAsText(file, "UTF-8"); }
1360       catch (err) { /* nothing to do */ };
1361       uploadBox.style.display = "none";
1362    }
1363 }
1364
1365 function openDialog()
1366 {
1367         callback = function (fname) { retrieveFile(fname); };
1368         showLibrary("Open file", callback, openDialog);
1369 }
1370
1371 function saveDialog()
1372 {
1373         callback = function (fname) {
1374           abortDialog("dialogBox");
1375           saveFile(fname,
1376                    (locked.innerHTML.html_to_matita()).sescape(),
1377                    (unlocked.innerHTML.html_to_matita()).sescape(),
1378                    false,saveDialog);
1379         };
1380         showLibrary("Save file as", callback, saveDialog);
1381 }
1382
1383 function newDialog()
1384 {
1385         callback = function (fname) {
1386           abortDialog("dialogBox");
1387           saveFile(fname,"",
1388                    "(* new script *)",
1389                    false,newDialog,true);
1390         };
1391         showLibrary("Create new file", callback, newDialog);
1392 }
1393
1394
1395 function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog,reloadFile)
1396 {
1397         if (!is_defined(reloadFile)) { reloadFile = true };
1398         if (!is_defined(fname)) {
1399             fname = current_fname;
1400             lockedtxt = (locked.innerHTML.html_to_matita()).sescape();
1401             unlockedtxt = (unlocked.innerHTML.html_to_matita()).sescape();
1402             force = true;
1403             // when force is true, reloadDialog is not needed
1404         }
1405         processor = function(xml) {
1406                 if (is_defined(xml)) {
1407                   if (xml.childNodes[0].textContent != "ok") {
1408                     if (confirm("File already exists. All existing data will be lost.\nDo you want to proceed anyway?")) {
1409                        saveFile(fname,lockedtxt,unlockedtxt,true,reloadDialog,reloadFile);
1410                     } else {
1411                       reloadDialog();
1412                     }
1413                   } else {
1414                     changeFile(fname);
1415                     debug("file saved!");
1416                     if (reloadFile) { retrieveFile(fname); }
1417                   }
1418                 } else {
1419                         error("save file failed");
1420                 }
1421                 resume();
1422         };
1423         if (is_defined(fname)) {
1424           pause();
1425           callServer("save",processor,"file=" + escape(fname) +
1426                                     "&locked=" + lockedtxt +
1427                                     "&unlocked=" + unlockedtxt +
1428                                     "&force=" + force);
1429         }
1430         else { error("no file selected"); }
1431 }
1432
1433 function createDir() {
1434    abortDialog("dialogBox");
1435    dirname = prompt("New directory name:\ncic:/matita/","newdir");
1436    if (dirname != null) {
1437         processor = function(xml) {
1438                 if (is_defined(xml)) {
1439                   if (xml.childNodes[0].textContent != "ok") {
1440                       alert("An error occurred :-(");
1441                   }
1442                 } else {
1443                       alert("An error occurred :-(");
1444                 }
1445                 resume();
1446                 dialogBox.reload();
1447         };
1448         pause();
1449         callServer("save",processor,"file=" + escape(dirname) +
1450                                     "&locked=&unlocked=&force=false&dir=true");
1451    } else {
1452       dialogBox.reload();
1453    }
1454 }
1455
1456 function commitAll()
1457 {
1458         processor = function(xml) {
1459                 if (xml.getElementsByTagName("details").length > 0) {
1460                         debug(xml.getElementsByTagName("details")[0].textContent);
1461                         alert("Commit executed: see details in the log.\n\n" +
1462                               "NOTICE: this message does NOT imply (yet) that the commit was successful.");
1463                 } else {
1464                         alert("Commit denied.\nPermission to commit and update is provided by the Matita team upon request.");
1465                 }
1466                 resume();
1467         };
1468         pause();
1469         callServer("commit",processor);
1470 }
1471
1472 function updateAll()
1473 {
1474         processor = function(xml) {
1475                 if (xml.getElementsByTagName("details").length > 0) {
1476                         alert("Update executed.\n\n" +
1477                               "Details:\n" +
1478                               xml.getElementsByTagName("details")[0].textContent);
1479                 } else {
1480                         alert("Update denied.\nPermission to commit and update is provided by the Matita team upon request.");
1481                 }
1482                 resume();
1483         };
1484         pause();
1485         callServer("update",processor);
1486 }
1487
1488 var goalcell;
1489
1490 function hideSequent() {
1491         matita.proofMode = false;
1492         updateSide();
1493 }
1494
1495 function showSequent() {
1496         matita.proofMode = true;
1497         updateSide();
1498 }
1499
1500 function showDialog(title,content,callback) {
1501   dialogTitle.innerHTML = title;
1502   dialogContent.innerHTML = content;
1503   dialogBox.callback = callback;
1504
1505   //Get the screen height and width
1506   var maskHeight = $(document).height();
1507   var maskWidth = $(window).width();
1508
1509   //Set heigth and width to mask to fill up the whole screen
1510   $('#mask').css({'width':maskWidth,'height':maskHeight});
1511
1512   //transition effect
1513   $('#mask').fadeIn(100);
1514   $('#mask').fadeTo(200,0.8);
1515
1516   //Get the window height and width
1517   var winH = $(window).height();
1518   var winW = $(window).width();
1519
1520   //Set the popup window to center
1521   $('#dialogBox').css('top',  winH/2-$('#dialogBox').height()/2);
1522   $('#dialogBox').css('left', winW/2-$('#dialogBox').width()/2);
1523
1524   //transition effect
1525   $('#dialogBox').fadeIn(200);
1526
1527   dialogBox.style.display = "block";
1528 }
1529
1530 function abortDialog(dialog) {
1531   document.getElementById(dialog).style.display = "none";
1532   $('#mask').hide();
1533 }
1534
1535 function removeElement(id) {
1536   var element = document.getElementById(id);
1537   element.parentNode.removeChild(element);
1538 }
1539
1540 var savedsc;
1541 var savedso;
1542
1543 function getCursorPos() {
1544   var cursorPos;
1545   if (window.getSelection) {
1546     var selObj = window.getSelection();
1547     savedRange = selObj.getRangeAt(0);
1548     savedsc = savedRange.startContainer;
1549     savedso = savedRange.startOffset;
1550     //cursorPos =  findNode(selObj.anchorNode.parentNode.childNodes, selObj.anchorNode) + selObj.anchorOffset;
1551     cursorPos =  findNode(unlocked.childNodes, selObj.anchorNode,0) + selObj.anchorOffset;
1552     /* FIXME the following works wrong in Opera when the document is longer than 32767 chars */
1553     return(cursorPos);
1554   }
1555   else if (document.selection) {
1556     savedRange = document.selection.createRange();
1557     var bookmark = savedRange.getBookmark();
1558     /* FIXME the following works wrong when the document is longer than 65535 chars */
1559     cursorPos = bookmark.charCodeAt(2) - 11; /* Undocumented function [3] */
1560     return(cursorPos);
1561   }
1562 }
1563
1564 function findNode(list, node, acc) {
1565   for (var i = 0; i < list.length; i++) {
1566     if (list[i] == node) {
1567    //   debug("success " + i);
1568       return acc;
1569     }
1570     if (list[i].hasChildNodes()) {
1571        try {
1572    //      debug("recursion on node " + i);
1573          return (findNode(list[i].childNodes,node,acc))
1574        }
1575        catch (e) { /* debug("recursion failed"); */ }
1576     }
1577     sandbox = document.getElementById("sandbox");
1578     dup = list[i].cloneNode(true);
1579     sandbox.appendChild(dup);
1580 //    debug("fail " + i + ": " + sandbox.innerHTML);
1581     acc += sandbox.innerHTML.html_to_matita().length;
1582     sandbox.removeChild(dup);
1583   }
1584   throw "not found";
1585 }
1586
1587 function test () {
1588   debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos()));
1589 }
1590
1591 function get_checked_index(name) {
1592         var radios = document.getElementsByName(name);
1593         for (i = 0; i < radios.length; i++) {
1594             if (radios[i].checked) {
1595                     return i;
1596             }
1597         }
1598         return null;
1599 }
1600
1601 function cancel_disambiguate() {
1602         matita.disambMode = false;
1603         resume();
1604         // enable_toparea();
1605         // enable_editing();
1606         strip_tags("span","error");
1607         updateSide();
1608 }
1609
1610 function do_disambiguate() {
1611         var i = get_checked_index("interpr");
1612         if (i != null) {
1613             var pre = matita.unlockedbackup
1614                       .substring(0,matita.ambiguityStart).matita_to_html();
1615             var mid = matita.unlockedbackup
1616                       .substring(matita.ambiguityStart,matita.ambiguityStop)
1617                       .matita_to_html();
1618             var post = matita.unlockedbackup
1619                        .substring(matita.ambiguityStop).matita_to_html();
1620
1621             var href = matita.interpretations[i].href;
1622             var title = matita.interpretations[i].title;
1623
1624             if (is_defined(title)) {
1625                 mid = "<A href=\"" + href + "\" title=\"" + title + "\">" + mid + "</A>";
1626             } else {
1627                 mid = "<A href=\"" + href + "\">" + mid + "</A>";
1628             }
1629
1630             unlocked.innerHTML = pre + mid + post;
1631
1632             matita.disambMode = false;
1633             enable_toparea();
1634             enable_editing();
1635             updateSide();
1636         }
1637 }
1638
1639 function do_showerror() {
1640         var i = get_checked_index("choice");
1641         if (i != null) {
1642             var pre = matita.unlockedbackup
1643                       .substring(0,matita.ambiguityStart).matita_to_html();
1644             var mid = matita.unlockedbackup
1645                       .substring(matita.ambiguityStart,matita.ambiguityStop)
1646                       .matita_to_html();
1647             var post = matita.unlockedbackup
1648                        .substring(matita.ambiguityStop).matita_to_html();
1649
1650             var href = matita.interpretations[i].href;
1651             var title = matita.interpretations[i].title;
1652
1653             if (is_defined(title)) {
1654                 mid = "<A href=\"" + href + "\" title=\"" + title + "\">" + mid + "</A>";
1655             } else {
1656                 mid = "<A href=\"" + href + "\">" + mid + "</A>";
1657             }
1658
1659             unlocked.innerHTML = pre + mid + post;
1660
1661         }
1662 }
1663
1664 function readCookie(name) {
1665         var nameEQ = name + "=";
1666         var ca = document.cookie.split(';');
1667         for(var i=0;i < ca.length;i++) {
1668                 var c = ca[i];
1669                 while (c.charAt(0)==' ') c = c.substring(1,c.length);
1670                 if (c.indexOf(nameEQ) == 0) return c.substring(nameEQ.length,c.length);
1671         }
1672         return null;
1673 }
1674
1675 function delete_cookie ( cookie_name )
1676 {
1677   var cookie_date = new Date();  // current date & time
1678   cookie_date.setTime ( cookie_date.getTime() - 1 );
1679   document.cookie = cookie_name += "=; expires=" + cookie_date.toGMTString();
1680 }
1681
1682 function delete_session()
1683 {
1684         delete_cookie("session");
1685 }
1686
1687 function disable_toparea() {
1688         var offset = $('#toparea').offset();
1689         $('#whitemask').css('top',offset.top);
1690         $('#whitemask').css('left',offset.left);
1691         $('#whitemask').css('width',$('#toparea').outerWidth() + "px");
1692         $('#whitemask').css('height',$('#toparea').outerHeight() + "px");
1693         $('#whitemask').fadeTo('fast',0.7);
1694 }
1695
1696 function enable_toparea() {
1697         $('#whitemask').hide();
1698 }
1699
1700 function disable_editing() {
1701         unlocked.contentEditable = false;
1702 }
1703
1704 function enable_editing() {
1705         unlocked.contentEditable = true;
1706 }
1707
1708 function pause()
1709 {
1710         // advanceButton.disabled = true;
1711         // retractButton.disabled = true;
1712         // cursorButton.disabled = true;
1713         // bottomButton.disabled = true;
1714         disable_toparea();
1715         disable_editing();
1716 }
1717
1718 function resume()
1719 {
1720         // advanceButton.disabled = false;
1721         // retractButton.disabled = false;
1722         // cursorButton.disabled = false;
1723         // bottomButton.disabled = false;
1724         if (!matita.disambMode) {
1725                 enable_toparea();
1726                 enable_editing();
1727         }
1728 }
1729
1730 function test()
1731 {
1732         xx.onclick();
1733 }