Made GUISimulatorUpdatesTable traversable with the Up and Down arrow keys when in focus, and also allows Enter to execute the update when in focus. Table has focus by default.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@204 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/userinterface/simulator/GUISimulator.java

@@ -38,6 +38,7 @@ import userinterface.properties.*;
 import userinterface.simulator.GUIViewDialog.RewardListItem;
 import userinterface.simulator.networking.*;
 import java.awt.event.*;
+
 import javax.swing.event.*;
 
 /**
@@ -127,7 +128,21 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 				if (e.getClickCount() == 2 && currentUpdatesTable.isEnabled())
 				{
 					a_manualUpdate();
+					currentUpdatesTable.requestFocus();
+				}
+			}
+		});
+		
+		currentUpdatesTable.addKeyListener(new KeyAdapter() 
+		{						
+			public void keyPressed(KeyEvent e) 
+			{
+				if (e.getKeyCode() == KeyEvent.VK_ENTER && currentUpdatesTable.isEnabled())
+				{
+					a_manualUpdate();
+					currentUpdatesTable.requestFocus();
 				}
+					
 			}
 		});
 		
@@ -171,6 +186,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 		getPrism().getSettings().setFileSelector(PrismSettings.SIMULATOR_NETWORK_FILE, netEdit );
 		
 		autoTimeCheck.setSelected(true);
+		currentUpdatesTable.requestFocus();
 	}
 	
 	public void setGUIProb(GUIMultiProperties guiProp)

prism/src/userinterface/simulator/GUISimulatorUpdatesTable.java

@@ -55,16 +55,16 @@ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionLis
     /** Creates a new instance of GUISimulatorUpdatesTable */
     public GUISimulatorUpdatesTable(GUISimulator.UpdateTableModel utm, GUISimulator sim)
     {
-	super(utm);
-	this.sim = sim;
-	this.utm = utm;
-	
-	this.getSelectionModel().addListSelectionListener(this);
-	
-	setColumnSelectionAllowed(false);
-	getSelectionModel().setSelectionMode(ListSelectionModel.SINGLE_SELECTION); 
-	
-	headerModel = new UpdateHeaderListModel();
+		super(utm);
+		this.sim = sim;
+		this.utm = utm;
+		
+		this.getSelectionModel().addListSelectionListener(this);
+		
+		setColumnSelectionAllowed(false);
+		getSelectionModel().setSelectionMode(ListSelectionModel.SINGLE_SELECTION); 
+		
+		headerModel = new UpdateHeaderListModel();
 		JList rowHeader = new JList(headerModel);
 	
 		rowHeader.setBackground(new JPanel().getBackground());
@@ -78,10 +78,52 @@ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionLis
 	
 		this.header = rowHeader;
 	
-	setDefaultRenderer(Object.class, new UpdateTableRenderer());
+		setDefaultRenderer(Object.class, new UpdateTableRenderer());
+	
 	
+		setAutoResizeMode(JTable.AUTO_RESIZE_LAST_COLUMN);
+		
+		InputMap inputMap = new ComponentInputMap(this);
+		
+		inputMap.put(KeyStroke.getKeyStroke(KeyEvent.VK_DOWN, 0), "Down");
+		inputMap.put(KeyStroke.getKeyStroke(KeyEvent.VK_UP, 0), "Up");
+		
+		ActionMap actionMap = new ActionMap();
+		
+		actionMap.put("Down", new AbstractAction() 
+		{
+			public void actionPerformed(ActionEvent e) 
+			{
+				int selectedRow = GUISimulatorUpdatesTable.this.getSelectedRow();
+				if (selectedRow != -1)
+				{
+					if (selectedRow < GUISimulatorUpdatesTable.this.getRowCount() - 1)
+						GUISimulatorUpdatesTable.this.getSelectionModel().setSelectionInterval(selectedRow + 1, selectedRow + 1);
+					else
+						GUISimulatorUpdatesTable.this.getSelectionModel().setSelectionInterval(0, 0);
+				}
+			}
+		});		
+		
+		actionMap.put("Up", new AbstractAction() 
+		{
+			public void actionPerformed(ActionEvent e) 
+			{
+				int selectedRow = GUISimulatorUpdatesTable.this.getSelectedRow();
+				if (selectedRow != -1)
+				{
+					if (selectedRow >= 1)
+						GUISimulatorUpdatesTable.this.getSelectionModel().setSelectionInterval(selectedRow - 1, selectedRow - 1);
+					else
+						GUISimulatorUpdatesTable.this.getSelectionModel().setSelectionInterval(GUISimulatorUpdatesTable.this.getRowCount()-1, GUISimulatorUpdatesTable.this.getRowCount()-1);
+				}
+			}
+		});		
+		
+		this.setInputMap(JComponent.WHEN_FOCUSED, inputMap);
+		this.setActionMap(actionMap);
+		
 	
-	setAutoResizeMode(JTable.AUTO_RESIZE_LAST_COLUMN);
     }
     
     public void valueChanged(ListSelectionEvent e)