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