comparison lib/js/urweb.js @ 889:bcad392e288e

Tweaking demos a bit
author Adam Chlipala <adamc@hcoop.net>
date Fri, 17 Jul 2009 18:13:02 -0400
parents 0f7e2cca6d9b
children ae9e22822ec5
comparison
equal deleted inserted replaced
888:ba3569f4fe89 889:bcad392e288e
420 else 420 else
421 return null; 421 return null;
422 } 422 }
423 423
424 function uf(s) { 424 function uf(s) {
425 return escape(s).replace(new RegExp ("/", "g"), "%2F"); 425 return escape(s).replace(new RegExp ("/", "g"), "%2F").replace(new RegExp ("\\+", "g"), "%2B");
426 } 426 }
427 427
428 function uu(s) { 428 function uu(s) {
429 return unescape(s).replace(new RegExp ("\\+", "g"), " "); 429 return unescape(s);
430 } 430 }
431 431
432 432
433 433
434 // Remote calls 434 // Remote calls
562 if (xhr.status == 200) 562 if (xhr.status == 200)
563 isok = true; 563 isok = true;
564 } catch (e) { } 564 } catch (e) { }
565 565
566 if (isok) { 566 if (isok) {
567 var lines = xhr.responseText.split("\n"); 567 var text = xhr.responseText
568 if (text == "")
569 return;
570 var lines = text.split("\n");
571
568 if (lines.length < 2) { 572 if (lines.length < 2) {
569 discon(); 573 discon();
570 return; 574 return;
571 } 575 }
572 576
601 } 605 }
602 else { 606 else {
603 try { 607 try {
604 if (xhr.status != 0) 608 if (xhr.status != 0)
605 servErr("Error querying remote server for messages: " + xhr.status); 609 servErr("Error querying remote server for messages: " + xhr.status);
606 } catch (e) { servErr("Error querying remote server for messages"); } 610 } catch (e) { }
607 } 611 }
608 } 612 }
609 }; 613 };
610 614
611 onTimeout = function() { 615 onTimeout = function() {