Fix window closing.

[graphlib_java.git] / DrawingWindow.java

diff --git a/DrawingWindow.java b/DrawingWindow.java
index 3b42553..670c854 100644 (file)
--- a/DrawingWindow.java
+++ b/DrawingWindow.java
@@ -621,6 +621,8 @@ public class DrawingWindow {
         colorMap = Collections.unmodifiableMap(m);
     }
 
+    private static int instances = 0;
+
     private final String title; // window's title
     private JFrame frame;       // the frame (window)
     private DWPanel panel;      // the panel showing the image
@@ -630,19 +632,32 @@ public class DrawingWindow {
 
     // To be run on the Event Dispatching Thread
     void createGUI() {
+        DrawingWindow.instances++;
         panel = new DWPanel(this);
-
         frame = new JFrame(title);
         frame.add(panel);
         frame.pack();
         frame.setResizable(false);
         frame.setDefaultCloseOperation(JFrame.DISPOSE_ON_CLOSE);
-        frame.addKeyListener(panel);
+        frame.addKeyListener(new KeyAdapter(){
+                public void keyPressed(KeyEvent e) {
+                    if (e.getKeyCode() == KeyEvent.VK_ESCAPE) {
+                        closeGraph();
+                    }
+                }
+            });
+        frame.addWindowListener(new WindowAdapter(){
+                public void windowClosed(WindowEvent e) {
+                    // System.err.println("CLOSED: " + DrawingWindow.instances);
+                    if (--DrawingWindow.instances == 0)
+                        System.exit(0);
+                }
+            });
         frame.setLocationByPlatform(true);
         frame.setVisible(true);
     }
 
-    private class DWPanel extends JPanel implements KeyListener {
+    private class DWPanel extends JPanel {
 
         private static final long serialVersionUID = 0;
 
@@ -661,15 +676,5 @@ public class DrawingWindow {
                 g.drawImage(w.image, 0, 0, null);
             }
         }
-
-        public void keyPressed(KeyEvent e) {
-            if (e.getKeyCode() == KeyEvent.VK_ESCAPE) {
-                w.closeGraph();
-            }
-        }
-
-        public void keyReleased(KeyEvent e) { }
-        public void keyTyped(KeyEvent e) { }
-
     }
 }