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