Index: tools/memory_inspector/memory_inspector/frontends/www_content/js/webservice.js |
diff --git a/tools/memory_inspector/memory_inspector/frontends/www_content/js/webservice.js b/tools/memory_inspector/memory_inspector/frontends/www_content/js/webservice.js |
index 437d3a4bc38eaea0c9cb1ced5fa228a1ae5aee17..2967d66ae58083caeb136e4c9cf63417f56ca716 100644 |
--- a/tools/memory_inspector/memory_inspector/frontends/www_content/js/webservice.js |
+++ b/tools/memory_inspector/memory_inspector/frontends/www_content/js/webservice.js |
@@ -6,6 +6,8 @@ webservice = new (function() { |
this.AJAX_BASE_URL_ = '/ajax'; |
+this.onServerUnreachableOrTimeout = null; |
+ |
this.ajaxRequest = function(path, responseCallback, errorCallback, postArgs) { |
var reqType = postArgs ? 'POST' : 'GET'; |
var reqData = postArgs ? JSON.stringify(postArgs) : ''; |
@@ -23,6 +25,8 @@ this.ajaxRequest = function(path, responseCallback, errorCallback, postArgs) { |
console.log(xhr.responseText); |
if (errorCallback) |
errorCallback(xhr.status, xhr.responseText); |
+ if (xhr.readyState < 4 && this_.onServerUnreachableOrTimeout != null) |
+ webservice.onServerUnreachableOrTimeout(); |
} |
}); |
}; |