From 4a81939bf1b50f53e84a1f730bc441ed4a8ed9dd Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 8 May 2008 09:08:59 +0000
Subject: [PATCH] GUI bug fix: tidy closing of Property Details windows.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@786 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 .../properties/GUIMultiProperties.java        |  2 +-
 .../properties/GUIPropertyResultDialog.java   | 28 ++++++++++++-------
 2 files changed, 19 insertions(+), 11 deletions(-)

diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java
index eb981372..8d82204a 100644
--- a/prism/src/userinterface/properties/GUIMultiProperties.java
+++ b/prism/src/userinterface/properties/GUIMultiProperties.java
@@ -825,7 +825,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 				gp.setBeingEdited(true);
 				// Force repaint because we modified the GUIProperty directly
 				repaintList();
-				new GUIPropertyResultDialog(getGUI(), this, gp).show();
+				new GUIPropertyResultDialog(getGUI(), this, gp).display();
 			}
 		}
 	}
diff --git a/prism/src/userinterface/properties/GUIPropertyResultDialog.java b/prism/src/userinterface/properties/GUIPropertyResultDialog.java
index da728e36..41858a3a 100644
--- a/prism/src/userinterface/properties/GUIPropertyResultDialog.java
+++ b/prism/src/userinterface/properties/GUIPropertyResultDialog.java
@@ -103,7 +103,12 @@ public class GUIPropertyResultDialog extends javax.swing.JDialog
 		jPanel12 = new javax.swing.JPanel();
 		jPanel13 = new javax.swing.JPanel();
 
-		setDefaultCloseOperation(javax.swing.WindowConstants.DISPOSE_ON_CLOSE);
+        addWindowListener(new java.awt.event.WindowAdapter() {
+            public void windowClosing(java.awt.event.WindowEvent evt) {
+                closeDialog();
+            }
+        });
+        
 		jPanel2.setLayout(new java.awt.FlowLayout(java.awt.FlowLayout.RIGHT));
 
 		jButton1.setText("Okay");
@@ -257,20 +262,23 @@ public class GUIPropertyResultDialog extends javax.swing.JDialog
 
 	private void jButton1ActionPerformed(java.awt.event.ActionEvent evt)//GEN-FIRST:event_jButton1ActionPerformed
 	{//GEN-HEADEREND:event_jButton1ActionPerformed
-	gp.setBeingEdited(false);
-	gmp.repaintList();
-	setVisible(false);
-	dispose();
+		closeDialog();
 	}//GEN-LAST:event_jButton1ActionPerformed
 	
-  
-	public void show()
+	/** Closes the dialog */
+	private void closeDialog()
+	{
+		gp.setBeingEdited(false);
+		gmp.repaintList();
+		setVisible(false);
+		dispose();
+	}
+
+	public void display()
 	{
 		noOpen++;
 		setLocation(getX()+(noOpen*50), getY()+(noOpen*50));
-		
-		super.show();
-		
+		super.setVisible(true);
 	}
 	
 	public void dispose()