From 681350864f0426872e97fbfa58ab1b3683549d90 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 13 Jun 2012 22:05:47 +0000
Subject: [PATCH] Double click to zoom out in GUI graphs.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5356 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 .../userinterface/properties/GUIGraphHandler.java    | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/prism/src/userinterface/properties/GUIGraphHandler.java b/prism/src/userinterface/properties/GUIGraphHandler.java
index fb9f989a..ef8484e0 100644
--- a/prism/src/userinterface/properties/GUIGraphHandler.java
+++ b/prism/src/userinterface/properties/GUIGraphHandler.java
@@ -636,6 +636,16 @@ public class GUIGraphHandler extends JPanel implements MouseListener
 		}		
 	}
 	
+	public void mouseClicked(MouseEvent e)
+	{
+		// Zoom out on double click
+		if (e.getClickCount() == 2) {
+			if (e.getSource() instanceof Graph) {
+				((Graph) e.getSource()).restoreAutoBounds();
+			}
+		}
+	}
+	
 	public void mouseReleased(MouseEvent e) 
 	{ 
 		if(e.isPopupTrigger())
@@ -705,7 +715,7 @@ public class GUIGraphHandler extends JPanel implements MouseListener
 	}
 	
 	// don't implement these for tabs
-	public void mouseClicked(MouseEvent e) { }
+	//public void mouseClicked(MouseEvent e) { }
 	public void mouseEntered(MouseEvent e) { }
 	public void mouseExited(MouseEvent e)  { }