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