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 initialize()
  21 {
  22   if (readCookie("session") == null) {
  23     window.location = "/login.html"
  24   } else {
  25     locked = document.getElementById("locked");
  26     unlocked = document.getElementById("unlocked");
  27     workarea = document.getElementById("workarea");
  28     scriptcell = document.getElementById("scriptcell");
  29     goalcell = document.getElementById("goalcell");
  30     goals = document.getElementById("goals");
  31     goalview = document.getElementById("goalview");
  32     filename = document.getElementById("filename");
  33     logarea = document.getElementById("logarea");
  34     advanceButton = document.getElementById("advance");
  35     retractButton = document.getElementById("retract");
  36     cursorButton = document.getElementById("cursor");
  37     bottomButton = document.getElementById("bottom");
  38     dialogBox = document.getElementById("dialogBox");
  39     dialogTitle = document.getElementById("dialogTitle");
  40     dialogContent = document.getElementById("dialogContent");
  41
  42     // hide sequent view at start
  43     hideSequent();
  44
  45     // initialize keyboard events in the unlocked script
  46     init_keyboard(unlocked);
  47   }
  48 }
  49
  50 function init_keyboard(target)
  51 {
  52     if (target.addEventListener)
  53     {
  54 //       target.addEventListener("keydown",keydown,false);
  55        target.addEventListener("keypress",keypress,false);
  56 //       target.addEventListener("keyup",keyup,false);
  57 //       target.addEventListener("textInput",textinput,false);
  58     }
  59     else if (target.attachEvent)
  60     {
  61 //       target.attachEvent("onkeydown", keydown);
  62        target.attachEvent("onkeypress", keypress);
  63 //       target.attachEvent("onkeyup", keyup);
  64 //       target.attachEvent("ontextInput", textinput);
  65     }
  66     else
  67     {
  68 //       target.onkeydown= keydown;
  69        target.onkeypress= keypress;
  70 //       target.onkeyup= keyup;
  71 //       target.ontextinput= textinput;   // probably doesn't work
  72     }
  73
  74 }
  75
  76 function keyval(n)
  77 {
  78     if (n == null) return 'undefined';
  79     var s= '' + n;
  80     if (n >= 32 && n < 127) s+= ' (' + String.fromCharCode(n) + ')';
  81     while (s.length < 9) s+= ' ';
  82     return s;
  83 }
  84
  85 function string_of_key(n)
  86 {
  87     if (n == null) return 'undefined';
  88     return String.fromCharCode(n);
  89 }
  90
  91 function pressmesg(w,e)
  92 {
  93    debug(w + '  keyCode=' + keyval(e.keyCode) +
  94                  ' which=' + keyval(e.which) +
  95                  ' charCode=' + keyval(e.charCode) +
  96                  '\n          shiftKey='+e.shiftKey
  97               + ' ctrlKey='+e.ctrlKey
  98               + ' altKey='+e.altKey
  99               + ' metaKey='+e.metaKey);
 100 }
 101
 102 function suppressdefault(e,flag)
 103 {
 104    if (flag)
 105    {
 106        if (e.preventDefault) e.preventDefault();
 107        if (e.stopPropagation) e.stopPropagation();
 108    }
 109    return !flag;
 110 }
 111
 112 function restoreSelection(adjust) {
 113     unlocked.focus();
 114     if (savedRange != null) {
 115         if (window.getSelection)//non IE and there is already a selection
 116         {
 117             var s = window.getSelection();
 118             if (s.rangeCount > 0)
 119                 s.removeAllRanges();
 120             range = document.createRange();
 121             range.setStart(savedsc,savedso + adjust);
 122             range.collapse(true);
 123             s.addRange(range);
 124         }
 125         else
 126             if (document.createRange)//non IE and no selection
 127             {
 128                 window.getSelection().addRange(savedRange);
 129             }
 130             else
 131                 if (document.selection)//IE
 132                 {
 133                     savedRange.select();
 134                 }
 135     }
 136 }
 137
 138 function lookup_tex(texmacro)
 139 {
 140   texmacro = texmacro.substring(1);
 141   return unescape(macro2utf8[texmacro]);
 142 }
 143
 144 function keypress(e)
 145 {
 146    if (!e) e= event;
 147    pressmesg('keypress',e);
 148    var s = string_of_key(e.charCode);
 149    if (s == " ") {
 150         j = getCursorPos();
 151         i = unlocked.innerHTML.lastIndexOf('\\',j);
 152         if (i >= 0) {
 153           match = unlocked.innerHTML.substring(i,j);
 154           pre = unlocked.innerHTML.substring(0,i);
 155           post = unlocked.innerHTML.substring(j);
 156
 157           sym = lookup_tex(match);
 158           if (typeof sym != "undefined") {
 159              len1 = unlocked.innerText.length;
 160              unlocked.innerHTML = pre + sym + post;
 161              len2 = unlocked.innerText.length;
 162              restoreSelection(len2 - len1);
 163              return suppressdefault(e,true);
 164           }
 165           else {
 166              // restoreSelection(0);
 167              return suppressdefault(e,false);
 168           }
 169         }
 170         else return suppressdefault(e,false);
 171    } else {
 172         return suppressdefault(e,false);
 173    }
 174 }
 175
 176 function debug(txt)
 177 {
 178         // internet explorer (v.9) doesn't work with innerHTML
 179         // but google chrome's innerText is, in a sense, "write only"
 180         // what should we do?
 181         logarea.innerText = txt + "\n" + logarea.innerText;
 182 }
 183
 184 function listhd(l)
 185 {
 186         ar = l.split("#");
 187         debug("hd of '" + l + "' = '" + ar[0] + "'");
 188         return (ar[0]);
 189 }
 190
 191 function listtl(l)
 192 {
 193         i = l.indexOf("#");
 194         tl = l.substr(i+1);
 195         debug("tl of '" + l + "' = '" + tl + "'");
 196         return (tl);
 197 }
 198
 199 function listcons(x,l)
 200 {
 201         debug("cons '" + x + "' on '" + l + "'");
 202         return (x + "#" + l);
 203 }
 204
 205 function listnil()
 206 {
 207         return ("");
 208 }
 209
 210 function is_nil(l)
 211 {
 212         return (l == "");
 213 }
 214
 215 function fold_left (f,acc,l)
 216 {
 217         if (is_nil(l))
 218            { debug("'" + l + "' is fold end");
 219            return (acc); }
 220         else
 221            { debug("'" + l + "' is fold cons");
 222              return(fold_left (f,f(acc,(listhd(l))),listtl(l))); }
 223 }
 224
 225 function listiter (f,l)
 226 {
 227         if (is_nil(l))
 228         { debug("'" + l + "' is nil");
 229            return;
 230         }
 231         else
 232         {
 233            debug("'" + l + "' is not nil");
 234            f(listhd(l));
 235            listiter(f,listtl(l));
 236         }
 237 }
 238
 239 function listmap (f,l)
 240 {
 241         debug("listmap on " + l);
 242         if (is_nil(l))
 243            { debug("returning listnil");
 244              return(listnil());
 245            }
 246         else
 247            { debug("cons f(hd) map(f,tl)");
 248              return(f(listhd(l)) + "#" + listmap(f,listtl(l)));
 249            }
 250 }
 251
 252 var statements = listnil();
 253
 254 var goalarray;
 255 var metalist = listnil();
 256
 257 function pairmap (f,p)
 258 {
 259   debug("pairmap of '" + p + "'");
 260   ar = p.split("|");
 261   return (f(ar[0],ar[1]));
 262 }
 263
 264 function tripletmap (f,p)
 265 {
 266   debug("tripletmap of '" + p + "'");
 267   ar = p.split("|");
 268   return (f(ar[0],ar[1],ar[2]));
 269 }
 270
 271 function fst (p)
 272 {
 273   debug("fst");
 274   return (pairmap (function (a,b) { return (a); }, p));
 275 }
 276
 277 function p13 (p)
 278 {
 279   debug("p13");
 280   return (tripletmap (function (a,b,c) { return (a); }, p));
 281 }
 282
 283 function p23 (p)
 284 {
 285   debug("p23");
 286   return (tripletmap (function (a,b,c) { return (b); }, p));
 287 }
 288
 289 function p33 (p)
 290 {
 291   debug("f33");
 292   return (tripletmap (function (a,b,c) { return (c); }, p));
 293 }
 294
 295 function populate_goalarray(menv)
 296 {
 297   debug("metasenv.length = " + menv.length);
 298   if (menv.length == 0) {
 299       try {
 300           hideSequent();
 301       } catch (err) { };
 302   } else {
 303       showSequent();
 304       goalarray = new Array();
 305       metalist = listnil();
 306       var tmp_goallist = "";
 307       for (i = 0; i < menv.length; i++) {
 308         metano = menv[i].getAttribute("number");
 309         metaname = menv[i].childNodes[0].childNodes[0].data;
 310         goal = menv[i].childNodes[1].childNodes[0].data;
 311         debug ("found meta n. " + metano);
 312         debug ("found goal\nBEGIN" + goal + "\nEND");
 313         goalarray[metano] = goal;
 314         tmp_goallist = " <A href=\"javascript:switch_goal(" + metano + ")\">" + metaname + "</A>" + tmp_goallist;
 315         metalist = listcons(metano,metalist);
 316         debug ("goalarray[\"" + metano + "\"] = " + goalarray[metano]);
 317       }
 318       goals.innerHTML = tmp_goallist;
 319       debug("new metalist is '" + metalist + "'");
 320       if (is_nil(metalist)) {
 321         switch_goal();
 322       }
 323       else {
 324         switch_goal(listhd(metalist));
 325       }
 326   }
 327 }
 328
 329 function switch_goal(meta)
 330 {
 331   if (typeof meta == "undefined") {
 332     goalview.innerHTML = "";
 333   }
 334   else {
 335     debug("switch_goal " + meta + "\n" + goalarray[meta]);
 336     goalview.innerHTML = "<B>Goal ?" + meta + ":</B>\n\n" + goalarray[meta];
 337   }
 338 }
 339
 340 // the following is used to avoid escaping unicode, which results in
 341 // the server being unable to unescape the string
 342 String.prototype.sescape = function() {
 343         var patt1 = /%/gi;
 344         var patt2 = /=/gi;
 345         var patt3 = /&/gi;
 346         var patt4 = /\+/gi;
 347         var result = this;
 348         result = result.replace(patt1,"%25");
 349         result = result.replace(patt2,"%3D");
 350         result = result.replace(patt3,"%26");
 351         result = result.replace(patt4,"%2B");
 352         return (result);
 353 }
 354
 355 String.prototype.html_to_matita = function()
 356 {
 357         var patt1 = /<br(\/|)>/gi;
 358         var patt2 = /</gi
 359         var patt3 = />/gi
 360         var patt4 = /&lt;/gi;
 361         var patt5 = /&gt;/gi;
 362         var result = this;
 363         result = result.replace(patt1,"\n");
 364         result = result.replace(patt2,"\005");
 365         result = result.replace(patt3,"\006");
 366         result = result.replace(patt4,"<");
 367         result = result.replace(patt5,">");
 368         return (unescape(result));
 369 }
 370
 371 String.prototype.matita_to_html = function()
 372 {
 373         var patt1 = /</gi
 374         var patt2 = />/gi
 375         var patt3 = /\005/gi;
 376         var patt4 = /\006/gi;
 377         var result = this;
 378         result = result.replace(patt1,"&lt;");
 379         result = result.replace(patt2,"&gt;");
 380         result = result.replace(patt3,"<");
 381         result = result.replace(patt4,">");
 382         return (unescape(result));
 383 }
 384
 385 function pause()
 386 {
 387         advanceButton.disabled = true;
 388         retractButton.disabled = true;
 389         cursorButton.disabled = true;
 390         bottomButton.disabled = true;
 391 }
 392
 393 function resume()
 394 {
 395         advanceButton.disabled = false;
 396         retractButton.disabled = false;
 397         cursorButton.disabled = false;
 398         bottomButton.disabled = false;
 399 }
 400
 401 function is_defined(x)
 402 {
 403         return (typeof x != "undefined");
 404 }
 405
 406 /* servicename: name of the service being called
 407  * reqbody: text of the request
 408  * processResponse: processes the server response
 409  *     (takes the response text in input, undefined in case of error)
 410  */
 411 function callServer(servicename,processResponse,reqbody)
 412 {
 413         var req = null;
 414         // pause();
 415         if (window.XMLHttpRequest)
 416         {
 417                 req = new XMLHttpRequest();
 418         }
 419         else if (window.ActiveXObject)
 420         {
 421                 try {
 422                                 req = new ActiveXObject("Msxml2.XMLHTTP");
 423                 } catch (e)
 424                 {
 425                         try {
 426                                 req = new ActiveXObject("Microsoft.XMLHTTP");
 427                                 } catch (e) {}
 428                 }
 429         }
 430         req.onreadystatechange = function()
 431         {
 432
 433                 rs = req.readyState;
 434
 435                 if(rs == 4)
 436                 {
 437                         stat = req.status;
 438                         stxt = req.statusText;
 439                         if(stat == 200)
 440                         {
 441                           debug(req.responseText);
 442                           if (window.DOMParser) {
 443                             parser=new DOMParser();
 444                             xmlDoc=parser.parseFromString(req.responseText,"text/xml");
 445                           }
 446                           else // Internet Explorer
 447                           {
 448                             xmlDoc=new ActiveXObject("Microsoft.XMLDOM");
 449                             xmlDoc.async="false";
 450                             xmlDoc.loadXML(req.responseText);
 451                           }
 452                           processResponse(xmlDoc);
 453                         } else {
 454                           processResponse();
 455                         }
 456                 }
 457         };
 458         req.open("POST", servicename); // + escape(unlocked.innerHTML), true);
 459         req.setRequestHeader("Content-type","application/x-www-form-urlencoded");
 460         if (reqbody) {
 461                 req.send(reqbody);
 462         } else {
 463                 req.send();
 464         }
 465
 466 }
 467
 468 function advanceForm1()
 469 {
 470         processor = function(xml) {
 471                 if (is_defined(xml)) {
 472                         // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
 473                         parsed = xml.getElementsByTagName("parsed")[0];
 474                         len = parseInt(parsed.getAttribute("length"));
 475                         // len0 = unlocked.innerHTML.length;
 476                         unescaped = unlocked.innerHTML.html_to_matita();
 477                         parsedtxt = parsed.childNodes[0].nodeValue;
 478                         //parsedtxt = unescaped.substr(0,len);
 479                         unparsedtxt = unescaped.substr(len);
 480                         lockedbackup += parsedtxt;
 481                         locked.innerHTML = lockedbackup;
 482                         unlocked.innerHTML = unparsedtxt.matita_to_html();
 483                         // len1 = unlocked.innerHTML.length;
 484                         // len2 = len0 - len1;
 485                         len2 = parsedtxt.length;
 486                         metasenv = xml.getElementsByTagName("meta");
 487                         populate_goalarray(metasenv);
 488                         statements = listcons(len2,statements);
 489                         unlocked.scrollIntoView(true);
 490                 } else {
 491                         debug("advance failed");
 492                 }
 493                 resume();
 494         };
 495         pause();
 496         callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
 497
 498 }
 499
 500 function gotoBottom()
 501 {
 502         processor = function(xml) {
 503                 if (is_defined(xml)) {
 504                         // debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND");
 505                         parsed = xml.getElementsByTagName("parsed")[0];
 506                         len = parseInt(parsed.getAttribute("length"));
 507                         if (len > 0) {
 508                           // len0 = unlocked.innerHTML.length;
 509                           unescaped = unlocked.innerHTML.html_to_matita();
 510                           parsedtxt = parsed.childNodes[0].nodeValue;
 511                           //parsedtxt = unescaped.substr(0,len);
 512                           unparsedtxt = unescaped.substr(len);
 513                           lockedbackup += parsedtxt;
 514                           locked.innerHTML = lockedbackup; //.matita_to_html();
 515                           unlocked.innerHTML = unparsedtxt.matita_to_html();
 516                           // len1 = unlocked.innerHTML.length;
 517                           len2 = parsedtxt.length;
 518                           metasenv = xml.getElementsByTagName("meta");
 519                           populate_goalarray(metasenv);
 520                           if (len2 > 0)
 521                             statements = listcons(len2,statements);
 522                           unlocked.scrollIntoView(true);
 523                         }
 524                 } else {
 525                         debug("goto bottom failed");
 526                 }
 527                 resume();
 528         };
 529         pause();
 530         callServer("bottom",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
 531
 532 }
 533
 534
 535 function gotoPos(offset)
 536 {
 537         if (!is_defined(offset)) {
 538                 offset = getCursorPos();
 539         }
 540         processor = function(xml) {
 541                 if (is_defined(xml)) {
 542                         parsed = xml.getElementsByTagName("parsed")[0];
 543                         len = parseInt(parsed.getAttribute("length"));
 544                         // len0 = unlocked.innerHTML.length;
 545                         unescaped = unlocked.innerHTML.html_to_matita();
 546                         parsedtxt = parsed.childNodes[0].nodeValue;
 547                         //parsedtxt = unescaped.substr(0,len);
 548                         unparsedtxt = unescaped.substr(len);
 549                         lockedbackup += parsedtxt;
 550                         locked.innerHTML = lockedbackup; //.matita_to_html();
 551                         unlocked.innerHTML = unparsedtxt.matita_to_html();
 552                         // len1 = unlocked.innerHTML.length;
 553                         len2 = parsedtxt.length;
 554                         metasenv = xml.getElementsByTagName("meta");
 555                         // populate_goalarray(metasenv);
 556                         statements = listcons(len2,statements);
 557                         unlocked.scrollIntoView(true);
 558                         // la populate non andrebbe fatta a ogni passo
 559                         if (offset <= len) {
 560                                 populate_goalarray(metasenv);
 561                                 resume();
 562                         } else {
 563                                 gotoPos(offset - len);
 564                         }
 565                 } else {
 566                         unlocked.scrollIntoView(true);
 567                         populate_goalarray(metasenv);
 568                         resume();
 569                 }
 570         }
 571         pause();
 572         callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
 573 }
 574
 575 function retract()
 576 {
 577         processor = function(xml) {
 578                 if (typeof xml != "undefined") {
 579                         // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
 580                         statementlen = parseInt(listhd(statements));
 581                         statements = listtl(statements);
 582                         /*
 583                         lockedlen = locked.innerHTML.length - statementlen;
 584                         statement = locked.innerHTML.substr(lockedlen, statementlen);
 585                         locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
 586                         unlocked.innerHTML = statement + unlocked.innerHTML;
 587                         */
 588                         lockedlen = lockedbackup.length - statementlen;
 589                         statement = lockedbackup.substr(lockedlen, statementlen);
 590                         lockedbackup = lockedbackup.substr(0,lockedlen);
 591                         locked.innerHTML = lockedbackup;
 592                         unlocked.innerHTML = statement + unlocked.innerHTML;
 593                         metasenv = xml.getElementsByTagName("meta");
 594                         populate_goalarray(metasenv);
 595                         unlocked.scrollIntoView(true);
 596                 } else {
 597                         debug("retract failed");
 598                 }
 599                 resume();
 600         };
 601         debug("retract 1");
 602         pause();
 603         callServer("retract",processor);
 604         debug("retract 2");
 605 }
 606
 607 function openFile()
 608 {
 609         processor = function(xml)
 610         {
 611                 if (is_defined(xml)) {
 612                         lockedbackup = "";
 613                         locked.innerHTML = lockedbackup;
 614                         unlocked.innerHTML = xml.documentElement.textContent;
 615                 } else {
 616                         debug("file open failed");
 617                 }
 618         };
 619         callServer("open",processor,"file=" + escape(filename.value));
 620 }
 621
 622 function retrieveFile(thefile)
 623 {
 624         processor = function(xml)
 625         {
 626                 if (is_defined(xml)) {
 627                         lockedbackup = ""
 628                         locked.innerHTML = lockedbackup;
 629                         debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
 630                         unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
 631
 632                 } else {
 633                         debug("file open failed");
 634                 }
 635         };
 636         dialogBox.style.display = "none";
 637         current_fname = thefile;
 638         callServer("open",processor,"file=" + escape(thefile));
 639 }
 640
 641 function showLibrary()
 642 {
 643         var req = null;
 644         // pause();
 645         if (window.XMLHttpRequest)
 646         {
 647                 req = new XMLHttpRequest();
 648         }
 649         else if (window.ActiveXObject)
 650         {
 651                 try {
 652                                 req = new ActiveXObject("Msxml2.XMLHTTP");
 653                 } catch (e)
 654                 {
 655                         try {
 656                                 req = new ActiveXObject("Microsoft.XMLHTTP");
 657                                 } catch (e) {}
 658                 }
 659         }
 660         req.onreadystatechange = function()
 661         {
 662
 663                 rs = req.readyState;
 664
 665                 if(rs == 4)
 666                 {
 667                         stat = req.status;
 668                         stxt = req.statusText;
 669                         if(stat == 200)
 670                         {
 671                           debug(req.responseText);
 672                           showDialog("<H2>Library</H2>",req.responseText);
 673                         }
 674                 }
 675         };
 676         req.open("POST", "viewlib"); // + escape(unlocked.innerHTML), true);
 677         req.setRequestHeader("Content-type","application/x-www-form-urlencoded");
 678         req.send();
 679
 680 }
 681
 682 function saveFile()
 683 {
 684         processor = function(xml) {
 685                 if (is_defined(xml)) {
 686                         debug("file saved!");
 687                 } else {
 688                         debug("save file failed");
 689                 }
 690                 resume();
 691         };
 692         if (is_defined(current_fname)) {
 693           pause();
 694           callServer("save",processor,"file=" + escape(current_fname) +
 695                                     "&locked=" + (locked.innerHTML.html_to_matita()).sescape() +
 696                                     "&unlocked=" + (unlocked.innerHTML.html_to_matita()).sescape());
 697         }
 698         else { debug("no file selected"); }
 699 }
 700
 701 function commitAll()
 702 {
 703         processor = function(xml) {
 704                 if (is_defined(xml)) {
 705                         debug("commit succeeded(?)");
 706                 } else {
 707                         debug("commit failed!");
 708                 }
 709                 resume();
 710         };
 711         pause();
 712         callServer("commit",processor);
 713 }
 714
 715 var goalcell;
 716
 717 function hideSequent() {
 718   goalcell.parentNode.removeChild(goalcell);
 719   scriptcell.setAttribute("colspan","2");
 720 }
 721
 722 function showSequent() {
 723   scriptcell.setAttribute("colspan","1");
 724   workarea.appendChild(goalcell);
 725 }
 726
 727 function showDialog(title,content) {
 728   dialogTitle.innerHTML = title;
 729   dialogContent.innerHTML = content;
 730   dialogBox.style.display = "block";
 731 }
 732
 733 function removeElement(id) {
 734   var element = document.getElementById(id);
 735   element.parentNode.removeChild(element);
 736 }
 737
 738 var savedsc;
 739 var savedso;
 740
 741 function getCursorPos() {
 742   var cursorPos;
 743   if (window.getSelection) {
 744     var selObj = window.getSelection();
 745     savedRange = selObj.getRangeAt(0);
 746     savedsc = savedRange.startContainer;
 747     savedso = savedRange.startOffset;
 748     //cursorPos =  findNode(selObj.anchorNode.parentNode.childNodes, selObj.anchorNode) + selObj.anchorOffset;
 749     cursorPos =  findNode(unlocked.childNodes, selObj.anchorNode,0) + selObj.anchorOffset;
 750     /* FIXME the following works wrong in Opera when the document is longer than 32767 chars */
 751     return(cursorPos);
 752   }
 753   else if (document.selection) {
 754     savedRange = document.selection.createRange();
 755     var bookmark = savedRange.getBookmark();
 756     /* FIXME the following works wrong when the document is longer than 65535 chars */
 757     cursorPos = bookmark.charCodeAt(2) - 11; /* Undocumented function [3] */
 758     return(cursorPos);
 759   }
 760 }
 761
 762 function findNode(list, node, acc) {
 763   for (var i = 0; i < list.length; i++) {
 764     if (list[i] == node) {
 765    //   debug("success " + i);
 766       return acc;
 767     }
 768     if (list[i].hasChildNodes()) {
 769        try {
 770    //      debug("recursion on node " + i);
 771          return (findNode(list[i].childNodes,node,acc))
 772        }
 773        catch (e) { /* debug("recursion failed"); */ }
 774     }
 775     sandbox = document.getElementById("sandbox");
 776     dup = list[i].cloneNode(true);
 777     sandbox.appendChild(dup);
 778 //    debug("fail " + i + ": " + sandbox.innerHTML);
 779     acc += sandbox.innerHTML.length;
 780     sandbox.removeChild(dup);
 781   }
 782   throw "not found";
 783 }
 784
 785 function test () {
 786   debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos()));
 787 }
 788
 789 function readCookie(name) {
 790         var nameEQ = name + "=";
 791         var ca = document.cookie.split(';');
 792         for(var i=0;i < ca.length;i++) {
 793                 var c = ca[i];
 794                 while (c.charAt(0)==' ') c = c.substring(1,c.length);
 795                 if (c.indexOf(nameEQ) == 0) return c.substring(nameEQ.length,c.length);
 796         }
 797         return null;
 798 }
 799
 800 function delete_cookie ( cookie_name )
 801 {
 802   var cookie_date = new Date();  // current date & time
 803   cookie_date.setTime ( cookie_date.getTime() - 1 );
 804   document.cookie = cookie_name += "=; expires=" + cookie_date.toGMTString();
 805 }
 806
 807 function delete_session()
 808 {
 809         delete_cookie("session");
 810 }