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