matitaB/matita/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
  20 function text_of_html(h)
  21 {
  22   if(document.all) {
  23      return h.innerText;
  24   } else {
  25      return h.textContent;
  26   }
  27 }
  28
  29 function unescape_html(s)
  30 {
  31   u = document.getElementById("unescape");
  32   u.innerHTML = s;
  33   return text_of_html(u)
  34 }
  35
  36 function initialize()
  37 {
  38   if (readCookie("session") == null) {
  39     window.location = "/login.html"
  40   } else {
  41     locked = document.getElementById("locked");
  42     unlocked = document.getElementById("unlocked");
  43     workarea = document.getElementById("workarea");
  44     scriptcell = document.getElementById("scriptcell");
  45     goalcell = document.getElementById("goalcell");
  46     goals = document.getElementById("goals");
  47     goalview = document.getElementById("goalview");
  48     filename = document.getElementById("filename");
  49     logarea = document.getElementById("logarea");
  50     advanceButton = document.getElementById("advance");
  51     retractButton = document.getElementById("retract");
  52     cursorButton = document.getElementById("cursor");
  53     bottomButton = document.getElementById("bottom");
  54     dialogBox = document.getElementById("dialogBox");
  55     dialogTitle = document.getElementById("dialogTitle");
  56     dialogContent = document.getElementById("dialogContent");
  57
  58     // hide sequent view at start
  59     hideSequent();
  60
  61     // initialize keyboard events in the unlocked script
  62     init_keyboard(unlocked);
  63   }
  64 }
  65
  66 function init_keyboard(target)
  67 {
  68     if (target.addEventListener)
  69     {
  70 //       target.addEventListener("keydown",keydown,false);
  71        target.addEventListener("keypress",keypress,false);
  72 //       target.addEventListener("keyup",keyup,false);
  73 //       target.addEventListener("textInput",textinput,false);
  74     }
  75     else if (target.attachEvent)
  76     {
  77 //       target.attachEvent("onkeydown", keydown);
  78        target.attachEvent("onkeypress", keypress);
  79 //       target.attachEvent("onkeyup", keyup);
  80 //       target.attachEvent("ontextInput", textinput);
  81     }
  82     else
  83     {
  84 //       target.onkeydown= keydown;
  85        target.onkeypress= keypress;
  86 //       target.onkeyup= keyup;
  87 //       target.ontextinput= textinput;   // probably doesn't work
  88     }
  89
  90 }
  91
  92 function keyval(n)
  93 {
  94     if (n == null) return 'undefined';
  95     var s= '' + n;
  96     if (n >= 32 && n < 127) s+= ' (' + String.fromCharCode(n) + ')';
  97     while (s.length < 9) s+= ' ';
  98     return s;
  99 }
 100
 101 function string_of_key(n)
 102 {
 103     if (n == null) return 'undefined';
 104     return String.fromCharCode(n);
 105 }
 106
 107 function pressmesg(w,e)
 108 {
 109    debug(w + '  keyCode=' + keyval(e.keyCode) +
 110                  ' which=' + keyval(e.which) +
 111                  ' charCode=' + keyval(e.charCode) +
 112                  '\n          shiftKey='+e.shiftKey
 113               + ' ctrlKey='+e.ctrlKey
 114               + ' altKey='+e.altKey
 115               + ' metaKey='+e.metaKey);
 116 }
 117
 118 function suppressdefault(e,flag)
 119 {
 120    if (flag)
 121    {
 122        if (e.preventDefault) e.preventDefault();
 123        if (e.stopPropagation) e.stopPropagation();
 124    }
 125    return !flag;
 126 }
 127
 128 function restoreSelection(r) {
 129     unlocked.focus();
 130     if (r != null) {
 131         if (window.getSelection)//non IE and there is already a selection
 132         {
 133             var s = window.getSelection();
 134             if (s.rangeCount > 0)
 135                 s.removeAllRanges();
 136             s.addRange(r);
 137         }
 138         else
 139             if (document.createRange)//non IE and no selection
 140             {
 141                 window.getSelection().addRange(r);
 142             }
 143             else
 144                 if (document.selection)//IE
 145                 {
 146                     r.select();
 147                 }
 148     }
 149 }
 150
 151 function lookup_tex(texmacro)
 152 {
 153   texmacro = texmacro.substring(1);
 154   return unescape(macro2utf8[texmacro]);
 155 }
 156
 157 function keypress(e)
 158 {
 159    if (!e) e= event;
 160    pressmesg('keypress',e);
 161    var s = string_of_key(e.charCode);
 162    if (s == " ") {
 163         j = getCursorPos();
 164         i = unlocked.innerHTML.lastIndexOf('\\',j);
 165         if (i >= 0) {
 166           match = unlocked.innerHTML.substring(i,j);
 167           sym = unescape_html(lookup_tex(match));
 168           if (sym != "undefined") {
 169              if (window.getSelection) { // non IE
 170                 savedRange.setStart(savedsc,savedso - (j-i));
 171                 savedRange.deleteContents();
 172                 savedRange.insertNode(document.createTextNode(sym));
 173                 savedsc.parentNode.normalize();
 174                 if (savedRange.collapsed) { // Mozilla
 175                   savedRange.setEnd(savedsc,savedRange.endOffset + sym.length);
 176                 }
 177                 savedRange.collapse(false);
 178              } else {
 179                 savedRange.moveStart(i-j);
 180                 savedRange.text(sym);
 181                 savedRange.collapse(false);
 182              }
 183              restoreSelection(savedRange);
 184              return suppressdefault(e,true);
 185           }
 186           else {
 187              // restoreSelection(0);
 188              return suppressdefault(e,false);
 189           }
 190         }
 191         else return suppressdefault(e,false);
 192    } else {
 193         return suppressdefault(e,false);
 194    }
 195 }
 196
 197 var logtxt = "";
 198
 199 function debug(txt)
 200 {
 201         // internet explorer (v.9) doesn't work with innerHTML
 202         // but google chrome's innerText is, in a sense, "write only"
 203         // what should we do?
 204         // logarea.innerText = txt + "\n" + logarea.innerText;
 205         logtxt = logtxt + "\n" + txt;
 206 }
 207
 208 function showLog() {
 209   logWin = window.open( "", "Matita Log",
 210      "width=600,height=450,status,scrollbars,resizable,screenX=20,screenY=40,left=20,top=40");
 211   logWin.document.write('<html><head><title>Matita Log' + '</title></head>');
 212   logWin.document.write('<body><textarea style="width:100%;height:100%;">' +
 213     logtxt + '</textarea></body></html>');
 214   logWin.document.close();
 215 }
 216
 217 function listhd(l)
 218 {
 219         ar = l.split("#");
 220         debug("hd of '" + l + "' = '" + ar[0] + "'");
 221         return (ar[0]);
 222 }
 223
 224 function listtl(l)
 225 {
 226         i = l.indexOf("#");
 227         tl = l.substr(i+1);
 228         debug("tl of '" + l + "' = '" + tl + "'");
 229         return (tl);
 230 }
 231
 232 function listcons(x,l)
 233 {
 234         debug("cons '" + x + "' on '" + l + "'");
 235         return (x + "#" + l);
 236 }
 237
 238 function listnil()
 239 {
 240         return ("");
 241 }
 242
 243 function is_nil(l)
 244 {
 245         return (l == "");
 246 }
 247
 248 function fold_left (f,acc,l)
 249 {
 250         if (is_nil(l))
 251            { debug("'" + l + "' is fold end");
 252            return (acc); }
 253         else
 254            { debug("'" + l + "' is fold cons");
 255              return(fold_left (f,f(acc,(listhd(l))),listtl(l))); }
 256 }
 257
 258 function listiter (f,l)
 259 {
 260         if (is_nil(l))
 261         { debug("'" + l + "' is nil");
 262            return;
 263         }
 264         else
 265         {
 266            debug("'" + l + "' is not nil");
 267            f(listhd(l));
 268            listiter(f,listtl(l));
 269         }
 270 }
 271
 272 function listmap (f,l)
 273 {
 274         debug("listmap on " + l);
 275         if (is_nil(l))
 276            { debug("returning listnil");
 277              return(listnil());
 278            }
 279         else
 280            { debug("cons f(hd) map(f,tl)");
 281              return(f(listhd(l)) + "#" + listmap(f,listtl(l)));
 282            }
 283 }
 284
 285 var statements = listnil();
 286
 287 var goalarray;
 288 var metalist = listnil();
 289
 290 function pairmap (f,p)
 291 {
 292   debug("pairmap of '" + p + "'");
 293   ar = p.split("|");
 294   return (f(ar[0],ar[1]));
 295 }
 296
 297 function tripletmap (f,p)
 298 {
 299   debug("tripletmap of '" + p + "'");
 300   ar = p.split("|");
 301   return (f(ar[0],ar[1],ar[2]));
 302 }
 303
 304 function fst (p)
 305 {
 306   debug("fst");
 307   return (pairmap (function (a,b) { return (a); }, p));
 308 }
 309
 310 function p13 (p)
 311 {
 312   debug("p13");
 313   return (tripletmap (function (a,b,c) { return (a); }, p));
 314 }
 315
 316 function p23 (p)
 317 {
 318   debug("p23");
 319   return (tripletmap (function (a,b,c) { return (b); }, p));
 320 }
 321
 322 function p33 (p)
 323 {
 324   debug("f33");
 325   return (tripletmap (function (a,b,c) { return (c); }, p));
 326 }
 327
 328 function populate_goalarray(menv)
 329 {
 330   debug("metasenv.length = " + menv.length);
 331   if (menv.length == 0) {
 332       try {
 333           hideSequent();
 334       } catch (err) { };
 335   } else {
 336       showSequent();
 337       goalarray = new Array();
 338       metalist = listnil();
 339       var tmp_goallist = "";
 340       for (i = 0; i < menv.length; i++) {
 341         metano = menv[i].getAttribute("number");
 342         metaname = menv[i].childNodes[0].childNodes[0].data;
 343         goal = menv[i].childNodes[1].childNodes[0].data;
 344         debug ("found meta n. " + metano);
 345         debug ("found goal\nBEGIN" + goal + "\nEND");
 346         goalarray[metano] = goal;
 347         tmp_goallist = " <A href=\"javascript:switch_goal(" + metano + ")\">" + metaname + "</A>" + tmp_goallist;
 348         metalist = listcons(metano,metalist);
 349         debug ("goalarray[\"" + metano + "\"] = " + goalarray[metano]);
 350       }
 351       goals.innerHTML = tmp_goallist;
 352       debug("new metalist is '" + metalist + "'");
 353       if (is_nil(metalist)) {
 354         switch_goal();
 355       }
 356       else {
 357         switch_goal(listhd(metalist));
 358       }
 359   }
 360 }
 361
 362 function switch_goal(meta)
 363 {
 364   if (typeof meta == "undefined") {
 365     goalview.innerHTML = "";
 366   }
 367   else {
 368     debug("switch_goal " + meta + "\n" + goalarray[meta]);
 369     goalview.innerHTML = "<B>Goal ?" + meta + ":</B>\n\n" + goalarray[meta];
 370   }
 371 }
 372
 373 // the following is used to avoid escaping unicode, which results in
 374 // the server being unable to unescape the string
 375 String.prototype.sescape = function() {
 376         var patt1 = /%/gi;
 377         var patt2 = /=/gi;
 378         var patt3 = /&/gi;
 379         var patt4 = /\+/gi;
 380         var result = this;
 381         result = result.replace(patt1,"%25");
 382         result = result.replace(patt2,"%3D");
 383         result = result.replace(patt3,"%26");
 384         result = result.replace(patt4,"%2B");
 385         return (result);
 386 }
 387
 388 String.prototype.html_to_matita = function()
 389 {
 390         var patt1 = /<br(\/|)>/gi;
 391         var patt2 = /</gi
 392         var patt3 = />/gi
 393         var patt4 = /&lt;/gi;
 394         var patt5 = /&gt;/gi;
 395         var patt6 = /&nbsp;/gi;
 396         var result = this;
 397         result = result.replace(patt1,"\n");
 398         result = result.replace(patt2,"\005");
 399         result = result.replace(patt3,"\006");
 400         result = result.replace(patt4,"<");
 401         result = result.replace(patt5,">");
 402         result = result.replace(patt6," ");
 403         return (unescape(result));
 404 }
 405
 406 String.prototype.matita_to_html = function()
 407 {
 408         var patt1 = /</gi
 409         var patt2 = />/gi
 410         var patt3 = /\005/gi;
 411         var patt4 = /\006/gi;
 412         var result = this;
 413         result = result.replace(patt1,"&lt;");
 414         result = result.replace(patt2,"&gt;");
 415         result = result.replace(patt3,"<");
 416         result = result.replace(patt4,">");
 417         return (unescape(result));
 418 }
 419
 420 function pause()
 421 {
 422         advanceButton.disabled = true;
 423         retractButton.disabled = true;
 424         cursorButton.disabled = true;
 425         bottomButton.disabled = true;
 426 }
 427
 428 function resume()
 429 {
 430         advanceButton.disabled = false;
 431         retractButton.disabled = false;
 432         cursorButton.disabled = false;
 433         bottomButton.disabled = false;
 434 }
 435
 436 function is_defined(x)
 437 {
 438         return (typeof x != "undefined");
 439 }
 440
 441 /* servicename: name of the service being called
 442  * reqbody: text of the request
 443  * processResponse: processes the server response
 444  *     (takes the response text in input, undefined in case of error)
 445  */
 446 function callServer(servicename,processResponse,reqbody)
 447 {
 448         var req = null;
 449         // pause();
 450         if (window.XMLHttpRequest)
 451         {
 452                 req = new XMLHttpRequest();
 453         }
 454         else if (window.ActiveXObject)
 455         {
 456                 try {
 457                                 req = new ActiveXObject("Msxml2.XMLHTTP");
 458                 } catch (e)
 459                 {
 460                         try {
 461                                 req = new ActiveXObject("Microsoft.XMLHTTP");
 462                                 } catch (e) {}
 463                 }
 464         }
 465         req.onreadystatechange = function()
 466         {
 467
 468                 rs = req.readyState;
 469
 470                 if(rs == 4)
 471                 {
 472                         stat = req.status;
 473                         stxt = req.statusText;
 474                         if(stat == 200)
 475                         {
 476                           debug(req.responseText);
 477                           if (window.DOMParser) {
 478                             parser=new DOMParser();
 479                             xmlDoc=parser.parseFromString(req.responseText,"text/xml");
 480                           }
 481                           else // Internet Explorer
 482                           {
 483                             xmlDoc=new ActiveXObject("Microsoft.XMLDOM");
 484                             xmlDoc.async="false";
 485                             xmlDoc.loadXML(req.responseText);
 486                           }
 487                           processResponse(xmlDoc);
 488                         } else {
 489                           processResponse();
 490                         }
 491                 }
 492         };
 493         req.open("POST", servicename); // + escape(unlocked.innerHTML), true);
 494         req.setRequestHeader("Content-type","application/x-www-form-urlencoded");
 495         if (reqbody) {
 496                 req.send(reqbody);
 497         } else {
 498                 req.send();
 499         }
 500
 501 }
 502
 503 function advanceForm1()
 504 {
 505         processor = function(xml) {
 506                 if (is_defined(xml)) {
 507                         // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
 508                         parsed = xml.getElementsByTagName("parsed")[0];
 509                         len = parseInt(parsed.getAttribute("length"));
 510                         // len0 = unlocked.innerHTML.length;
 511                         unescaped = unlocked.innerHTML.html_to_matita();
 512                         parsedtxt = parsed.childNodes[0].nodeValue;
 513                         //parsedtxt = unescaped.substr(0,len);
 514                         unparsedtxt = unescaped.substr(len);
 515                         lockedbackup += parsedtxt;
 516                         locked.innerHTML = lockedbackup;
 517                         unlocked.innerHTML = unparsedtxt.matita_to_html();
 518                         // len1 = unlocked.innerHTML.length;
 519                         // len2 = len0 - len1;
 520                         len2 = parsedtxt.length;
 521                         metasenv = xml.getElementsByTagName("meta");
 522                         populate_goalarray(metasenv);
 523                         statements = listcons(len2,statements);
 524                         unlocked.scrollIntoView(true);
 525                 } else {
 526                         debug("advance failed");
 527                 }
 528                 resume();
 529         };
 530         pause();
 531         callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
 532
 533 }
 534
 535 function gotoBottom()
 536 {
 537         processor = function(xml) {
 538                 if (is_defined(xml)) {
 539                         // debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND");
 540                         parsed = xml.getElementsByTagName("parsed")[0];
 541                         len = parseInt(parsed.getAttribute("length"));
 542                         if (len > 0) {
 543                           // len0 = unlocked.innerHTML.length;
 544                           unescaped = unlocked.innerHTML.html_to_matita();
 545                           // not working in mozilla
 546                           // parsedtxt = parsed.childNodes[0].nodeValue;
 547                           parsedtxt = parsed.childNodes[0].wholeText;
 548                           //parsedtxt = unescaped.substr(0,len);
 549                           unparsedtxt = unescaped.substr(len);
 550                           lockedbackup += parsedtxt;
 551                           locked.innerHTML = lockedbackup; //.matita_to_html();
 552                           unlocked.innerHTML = unparsedtxt.matita_to_html();
 553                           // len1 = unlocked.innerHTML.length;
 554                           len2 = parsedtxt.length;
 555                           metasenv = xml.getElementsByTagName("meta");
 556                           populate_goalarray(metasenv);
 557                           if (len2 > 0)
 558                             statements = listcons(len2,statements);
 559                           unlocked.scrollIntoView(true);
 560                         }
 561                 } else {
 562                         debug("goto bottom failed");
 563                 }
 564                 resume();
 565         };
 566         pause();
 567         callServer("bottom",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
 568
 569 }
 570
 571
 572 function gotoTop()
 573 {
 574         processor = function(xml) {
 575                 if (is_defined(xml)) {
 576                   if (xml.childNodes[0].textContent != "ok") {
 577                      debug("goto top failed");
 578                   }
 579                   else
 580                         statements = listnil();
 581                         /*
 582                         lockedlen = locked.innerHTML.length - statementlen;
 583                         statement = locked.innerHTML.substr(lockedlen, statementlen);
 584                         locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
 585                         unlocked.innerHTML = statement + unlocked.innerHTML;
 586                         */
 587                         unlocked.innerHTML = lockedbackup + unlocked.innerHTML;
 588                         lockedbackup = "";
 589                         locked.innerHTML = lockedbackup;
 590                         hideSequent();
 591                         unlocked.scrollIntoView(true);
 592                 } else {
 593                         debug("goto top failed");
 594                 }
 595                 resume();
 596         };
 597         pause();
 598         callServer("top",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
 599
 600 }
 601 function gotoPos(offset)
 602 {
 603         if (!is_defined(offset)) {
 604                 offset = getCursorPos();
 605         }
 606         processor = function(xml) {
 607                 if (is_defined(xml)) {
 608                         parsed = xml.getElementsByTagName("parsed")[0];
 609                         len = parseInt(parsed.getAttribute("length"));
 610                         // len0 = unlocked.innerHTML.length;
 611                         unescaped = unlocked.innerHTML.html_to_matita();
 612                         parsedtxt = parsed.childNodes[0].nodeValue;
 613                         //parsedtxt = unescaped.substr(0,len);
 614                         unparsedtxt = unescaped.substr(len);
 615                         lockedbackup += parsedtxt;
 616                         locked.innerHTML = lockedbackup; //.matita_to_html();
 617                         unlocked.innerHTML = unparsedtxt.matita_to_html();
 618                         // len1 = unlocked.innerHTML.length;
 619                         len2 = parsedtxt.length;
 620                         metasenv = xml.getElementsByTagName("meta");
 621                         // populate_goalarray(metasenv);
 622                         statements = listcons(len2,statements);
 623                         unlocked.scrollIntoView(true);
 624                         // la populate non andrebbe fatta a ogni passo
 625                         if (offset <= len) {
 626                                 populate_goalarray(metasenv);
 627                                 resume();
 628                         } else {
 629                                 gotoPos(offset - len);
 630                         }
 631                 } else {
 632                         unlocked.scrollIntoView(true);
 633                         populate_goalarray(metasenv);
 634                         resume();
 635                 }
 636         }
 637         pause();
 638         callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
 639 }
 640
 641 function retract()
 642 {
 643         processor = function(xml) {
 644                 if (typeof xml != "undefined") {
 645                         // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
 646                         statementlen = parseInt(listhd(statements));
 647                         statements = listtl(statements);
 648                         /*
 649                         lockedlen = locked.innerHTML.length - statementlen;
 650                         statement = locked.innerHTML.substr(lockedlen, statementlen);
 651                         locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
 652                         unlocked.innerHTML = statement + unlocked.innerHTML;
 653                         */
 654                         lockedlen = lockedbackup.length - statementlen;
 655                         statement = lockedbackup.substr(lockedlen, statementlen);
 656                         lockedbackup = lockedbackup.substr(0,lockedlen);
 657                         locked.innerHTML = lockedbackup;
 658                         unlocked.innerHTML = statement + unlocked.innerHTML;
 659                         metasenv = xml.getElementsByTagName("meta");
 660                         populate_goalarray(metasenv);
 661                         unlocked.scrollIntoView(true);
 662                 } else {
 663                         debug("retract failed");
 664                 }
 665                 resume();
 666         };
 667         debug("retract 1");
 668         pause();
 669         callServer("retract",processor);
 670         debug("retract 2");
 671 }
 672
 673 function openFile()
 674 {
 675         processor = function(xml)
 676         {
 677                 if (is_defined(xml)) {
 678                         lockedbackup = "";
 679                         locked.innerHTML = lockedbackup;
 680                         unlocked.innerHTML = xml.documentElement.wholeText;
 681                 } else {
 682                         debug("file open failed");
 683                 }
 684         };
 685         callServer("open",processor,"file=" + escape(filename.value));
 686 }
 687
 688 function retrieveFile(thefile)
 689 {
 690         processor = function(xml)
 691         {
 692                 if (is_defined(xml)) {
 693                         current_fname = thefile;
 694                         lockedbackup = ""
 695                         locked.innerHTML = lockedbackup;
 696                         // code originally used in google chrome (problems with mozilla)
 697                         // debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
 698                         // unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
 699                         debug(xml.childNodes[0].textContent);
 700                         if (document.all) { // IE
 701                           unlocked.innerHTML = xml.childNodes[0].text;
 702                         } else {
 703                           unlocked.innerHTML = xml.childNodes[0].textContent;
 704                         }
 705
 706                 } else {
 707                         debug("file open failed");
 708                 }
 709         };
 710         dialogBox.style.display = "none";
 711         callServer("open",processor,"file=" + escape(thefile));
 712 }
 713
 714 function showLibrary(title,callback,reloadDialog)
 715 {
 716         var req = null;
 717         dialogBox.reload = reloadDialog;
 718         // pause();
 719         if (window.XMLHttpRequest)
 720         {
 721                 req = new XMLHttpRequest();
 722         }
 723         else if (window.ActiveXObject)
 724         {
 725                 try {
 726                                 req = new ActiveXObject("Msxml2.XMLHTTP");
 727                 } catch (e)
 728                 {
 729                         try {
 730                                 req = new ActiveXObject("Microsoft.XMLHTTP");
 731                                 } catch (e) {}
 732                 }
 733         }
 734         req.onreadystatechange = function()
 735         {
 736
 737                 rs = req.readyState;
 738
 739                 if(rs == 4)
 740                 {
 741                         stat = req.status;
 742                         stxt = req.statusText;
 743                         if(stat == 200)
 744                         {
 745                           debug(req.responseText);
 746                           showDialog("<H2>" + title + "</H2>",req.responseText, callback);
 747                         }
 748                 }
 749         };
 750         req.open("POST", "viewlib"); // + escape(unlocked.innerHTML), true);
 751         req.setRequestHeader("Content-type","application/x-www-form-urlencoded");
 752         req.send();
 753
 754 }
 755
 756 function uploadDialog()
 757 {
 758         uploadBox.style.display = "block";
 759 }
 760
 761 function uploadOK()
 762 {
 763    var file = document.getElementById("uploadFilename").files[0];
 764    if (file) {
 765        var filecontent = file.getAsText("UTF-8");
 766        locked.innerHTML = lockedbackup;
 767        unlocked.innerHTML = filecontent;
 768        uploadBox.style.display = "none";
 769    }
 770 //   if (file) {
 771 //      var reader = new FileReader();
 772 //      reader.readAsText(file, "UTF-8");
 773 //       reader.onloadend = function (evt) {
 774 //         lockedbackup = "";
 775 //           locked.innerHTML = lockedbackup
 776 //           unlocked.innerHTML = evt.target.result;
 777 //           uploadBox.style.display = "none";
 778 //       }
 779 //       reader.onerror = function (evt) {
 780 //         debug("file open failed");
 781 //           uploadBox.style.display = "none";
 782 //      }
 783 //   }
 784 }
 785
 786 function openDialog()
 787 {
 788         callback = function (fname) { retrieveFile(fname); };
 789         showLibrary("Open file", callback, openDialog);
 790 }
 791
 792 function saveDialog()
 793 {
 794         callback = function (fname) {
 795           dialogBox.style.display = "none";
 796           saveFile(fname,
 797                    (locked.innerHTML.html_to_matita()).sescape(),
 798                    (unlocked.innerHTML.html_to_matita()).sescape(),
 799                    false,saveDialog);
 800         };
 801         showLibrary("Save file as", callback, saveDialog);
 802 }
 803
 804 function newDialog()
 805 {
 806         callback = function (fname) {
 807           dialogBox.style.display = "none";
 808           saveFile(fname,"","",false,newDialog,true);
 809         };
 810         showLibrary("Create new file", callback, newDialog);
 811 }
 812
 813
 814 function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog,reloadFile)
 815 {
 816         if (!is_defined(reloadFile)) { reloadFile = true };
 817         if (!is_defined(fname)) {
 818             fname = current_fname;
 819             lockedtxt = (locked.innerHTML.html_to_matita()).sescape();
 820             unlockedtxt = (unlocked.innerHTML.html_to_matita()).sescape();
 821             force = true;
 822             // when force is true, reloadDialog is not needed
 823         }
 824         processor = function(xml) {
 825                 current_fname = fname;
 826                 if (is_defined(xml)) {
 827                   if (xml.childNodes[0].textContent != "ok") {
 828                     if (confirm("File already exists. All existing data will be lost.\nDo you want to proceed anyway?")) {
 829                        saveFile(fname,lockedtxt,unlockedtxt,true,reloadDialog,reloadFile);
 830                     } else {
 831                       reloadDialog();
 832                     }
 833                   } else {
 834                     current_fname = fname;
 835                     debug("file saved!");
 836                     if (reloadFile) { retrieveFile(fname); }
 837                   }
 838                 } else {
 839                         debug("save file failed");
 840                 }
 841                 resume();
 842         };
 843         if (is_defined(fname)) {
 844           pause();
 845           callServer("save",processor,"file=" + escape(fname) +
 846                                     "&locked=" + lockedtxt +
 847                                     "&unlocked=" + unlockedtxt +
 848                                     "&force=" + force);
 849         }
 850         else { debug("no file selected"); }
 851 }
 852
 853 function createDir() {
 854    abortDialog();
 855    dirname = prompt("New directory name:\ncic:/matita/","newdir");
 856    if (dirname != null) {
 857         processor = function(xml) {
 858                 if (is_defined(xml)) {
 859                   if (xml.childNodes[0].textContent != "ok") {
 860                       alert("An error occurred :-(");
 861                   }
 862                 } else {
 863                       alert("An error occurred :-(");
 864                 }
 865                 dialogBox.reload();
 866         };
 867         pause();
 868         callServer("save",processor,"file=" + escape(dirname) +
 869                                     "&locked=&unlocked=&force=false&dir=true");
 870    } else {
 871       dialogBox.reload();
 872    }
 873 }
 874
 875 function commitAll()
 876 {
 877         processor = function(xml) {
 878                 if (is_defined(xml)) {
 879                         debug(xml.getElementsByTagName("details")[0].textContent);
 880                         alert("Commit executed: see details in the log.\n\n" +
 881                               "NOTICE: this message does NOT imply (yet) that the commit was successful.");
 882                 } else {
 883                         alert("Commit failed!");
 884                 }
 885                 resume();
 886         };
 887         pause();
 888         callServer("commit",processor);
 889 }
 890
 891 function updateAll()
 892 {
 893         processor = function(xml) {
 894                 if (is_defined(xml)) {
 895                         alert("Update executed.\n\n" +
 896                               "Details:\n" +
 897                               xml.getElementsByTagName("details")[0].textContent);
 898                 } else {
 899                         alert("Update failed!");
 900                 }
 901                 resume();
 902         };
 903         pause();
 904         callServer("update",processor);
 905 }
 906
 907 var goalcell;
 908
 909 function hideSequent() {
 910   goalcell.style.display = "none";
 911   scriptcell.style.width = "100%";
 912   scriptcell.style.minWidth = "100%";
 913   scriptcell.style.maxWidth = "100%";
 914 }
 915
 916 function showSequent() {
 917   scriptcell.style.width = "67%";
 918   scriptcell.style.minWidth = "67%";
 919   scriptcell.style.maxWidth = "67%";
 920   goalcell.style.display = "inline-block";
 921 }
 922
 923 function showDialog(title,content,callback) {
 924   dialogTitle.innerHTML = title;
 925   dialogContent.innerHTML = content;
 926   dialogBox.callback = callback;
 927   dialogBox.style.display = "block";
 928 }
 929
 930 function abortDialog() {
 931   dialogBox.style.display = "none";
 932 }
 933
 934 function abortUpload() {
 935   uploadBox.style.display = "none";
 936 }
 937
 938 function removeElement(id) {
 939   var element = document.getElementById(id);
 940   element.parentNode.removeChild(element);
 941 }
 942
 943 var savedsc;
 944 var savedso;
 945
 946 function getCursorPos() {
 947   var cursorPos;
 948   if (window.getSelection) {
 949     var selObj = window.getSelection();
 950     savedRange = selObj.getRangeAt(0);
 951     savedsc = savedRange.startContainer;
 952     savedso = savedRange.startOffset;
 953     //cursorPos =  findNode(selObj.anchorNode.parentNode.childNodes, selObj.anchorNode) + selObj.anchorOffset;
 954     cursorPos =  findNode(unlocked.childNodes, selObj.anchorNode,0) + selObj.anchorOffset;
 955     /* FIXME the following works wrong in Opera when the document is longer than 32767 chars */
 956     return(cursorPos);
 957   }
 958   else if (document.selection) {
 959     savedRange = document.selection.createRange();
 960     var bookmark = savedRange.getBookmark();
 961     /* FIXME the following works wrong when the document is longer than 65535 chars */
 962     cursorPos = bookmark.charCodeAt(2) - 11; /* Undocumented function [3] */
 963     return(cursorPos);
 964   }
 965 }
 966
 967 function findNode(list, node, acc) {
 968   for (var i = 0; i < list.length; i++) {
 969     if (list[i] == node) {
 970    //   debug("success " + i);
 971       return acc;
 972     }
 973     if (list[i].hasChildNodes()) {
 974        try {
 975    //      debug("recursion on node " + i);
 976          return (findNode(list[i].childNodes,node,acc))
 977        }
 978        catch (e) { /* debug("recursion failed"); */ }
 979     }
 980     sandbox = document.getElementById("sandbox");
 981     dup = list[i].cloneNode(true);
 982     sandbox.appendChild(dup);
 983 //    debug("fail " + i + ": " + sandbox.innerHTML);
 984     acc += sandbox.innerHTML.length;
 985     sandbox.removeChild(dup);
 986   }
 987   throw "not found";
 988 }
 989
 990 function test () {
 991   debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos()));
 992 }
 993
 994 function readCookie(name) {
 995         var nameEQ = name + "=";
 996         var ca = document.cookie.split(';');
 997         for(var i=0;i < ca.length;i++) {
 998                 var c = ca[i];
 999                 while (c.charAt(0)==' ') c = c.substring(1,c.length);
1000                 if (c.indexOf(nameEQ) == 0) return c.substring(nameEQ.length,c.length);
1001         }
1002         return null;
1003 }
1004
1005 function delete_cookie ( cookie_name )
1006 {
1007   var cookie_date = new Date();  // current date & time
1008   cookie_date.setTime ( cookie_date.getTime() - 1 );
1009   document.cookie = cookie_name += "=; expires=" + cookie_date.toGMTString();
1010 }
1011
1012 function delete_session()
1013 {
1014         delete_cookie("session");
1015 }