From: Leif Åstrand <leif@vaadin.com>
Date: Fri, 19 Jul 2013 11:36:56 +0000 (+0300)
Subject: Close PushRequestHandler when VaadinServlet is destroyed (#11878)
X-Git-Tag: 7.1.2~23
X-Git-Url: https://source.dussan.org/?a=commitdiff_plain;h=9c8eb70dd54c1ba56d02111b9246a7767e1a0442;p=vaadin-framework.git

Close PushRequestHandler when VaadinServlet is destroyed (#11878)

Should be implemented using ServiceDestoryListener in Vaadin 7.2

Merge: no

Change-Id: Ibb4d37f1f95c56b80111df3a3217076af18dd93d
---

diff --git a/server/src/com/vaadin/server/VaadinServlet.java b/server/src/com/vaadin/server/VaadinServlet.java
index 803a903341..c16be33de2 100644
--- a/server/src/com/vaadin/server/VaadinServlet.java
+++ b/server/src/com/vaadin/server/VaadinServlet.java
@@ -43,6 +43,7 @@ import javax.servlet.http.HttpServletResponse;
 import com.vaadin.annotations.VaadinServletConfiguration;
 import com.vaadin.annotations.VaadinServletConfiguration.InitParameterName;
 import com.vaadin.sass.internal.ScssStylesheet;
+import com.vaadin.server.communication.PushRequestHandler;
 import com.vaadin.server.communication.ServletUIInitHandler;
 import com.vaadin.shared.JsonConstants;
 import com.vaadin.ui.UI;
@@ -1076,6 +1077,17 @@ public class VaadinServlet extends HttpServlet implements Constants {
         return u;
     }
 
+    @Override
+    public void destroy() {
+        super.destroy();
+
+        for (RequestHandler handler : getService().getRequestHandlers()) {
+            if (handler instanceof PushRequestHandler) {
+                ((PushRequestHandler) handler).destroy();
+            }
+        }
+    }
+
     /**
      * Escapes characters to html entities. An exception is made for some
      * "safe characters" to keep the text somewhat readable.