From aa807d3ab3f6ee2d2ae8c19a133748ededd5cbfe Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 10 Jun 2013 23:03:47 +0000 Subject: [PATCH] Small improvements to usability of the GUI simulator transition table. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6886 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/images/smallItemSelectedDisabled.png | Bin 0 -> 231 bytes .../userinterface/simulator/GUISimulator.java | 8 ++++---- .../simulator/GUISimulatorUpdatesTable.java | 15 +++++++-------- 3 files changed, 11 insertions(+), 12 deletions(-) create mode 100644 prism/images/smallItemSelectedDisabled.png diff --git a/prism/images/smallItemSelectedDisabled.png b/prism/images/smallItemSelectedDisabled.png new file mode 100644 index 0000000000000000000000000000000000000000..70f5367e15264970ffbb5946c357ece4c97638ca GIT binary patch literal 231 zcmeAS@N?(olHy`uVBq!ia0vp^93afW0wnX;%77#TQFdgVmyJuzfN6D>MF&u*!qdeugyVX0LIOwsy8DmRPcX3h@bKi{ zc)DlndX}hztPzrRMkl;y%5|*uNo?WTlUQ-`Lwo4X-ty`-0^H2Z+=q+X?0Ir{f_P%= zBmQkPFxX&FV6efErT5YOiHi Uz5080HqZ?Wp00i_>zopr0PKWL;Q#;t literal 0 HcmV?d00001 diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index d9a9bf38..dc792d8d 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -132,7 +132,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect currentUpdatesTable.requestFocus(); } else if (e.getClickCount() == 2 && !currentUpdatesTable.isEnabled()) { GUISimulator.this.warning("Simulation", - "You cannot continue exploration from the state that is current selected.\nSelect the last state in the path table to continue"); + "These are updates from earlier in the path.\nSelect the last state in the path table to continue exploration"); } } }); @@ -928,6 +928,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect typeBacktrackCombo.setEnabled(pathActive); currentUpdatesTable.setEnabled(pathActive && !computing); + currentUpdatesTable.setToolTipText(currentUpdatesTable.isEnabled() ? "Double click on an update to manually execute it" : null); autoTimeCheck.setEnabled(pathActive && parsedModel != null && parsedModel.getModelType().continuousTime()); //resetPathButton.setEnabled(pathActive && !computing); @@ -938,8 +939,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect //newPathFromState.setEnabled(parsedModel != null && !computing); //newPathButton.setEnabled(parsedModel != null && !computing); - currentUpdatesTable.setEnabled(pathActive); - modelType.setEnabled(parsedModel != null); modelTypeLabel.setEnabled(parsedModel != null); @@ -1363,7 +1362,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect manualUpdateTableScrollPane.setBorder(javax.swing.BorderFactory.createEmptyBorder(0, 0, 0, 0)); currentUpdatesTable.setModel(new javax.swing.table.DefaultTableModel(new Object[][] { { null, null, null, null }, { null, null, null, null }, { null, null, null, null }, { null, null, null, null } }, new String[] { "Title 1", "Title 2", "Title 3", "Title 4" })); - currentUpdatesTable.setToolTipText("Double click on an update to manually execute the update"); manualUpdateTableScrollPane.setViewportView(currentUpdatesTable); innerManualUpdatesPanel.add(manualUpdateTableScrollPane, java.awt.BorderLayout.CENTER); @@ -2193,6 +2191,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect fireTableDataChanged(); currentUpdatesTable.setEnabled(true); + currentUpdatesTable.setToolTipText("Double click on an update to manually execute it"); if (getRowCount() > 0) { currentUpdatesTable.getSelectionModel().setSelectionInterval(0, 0); @@ -2215,6 +2214,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect fireTableDataChanged(); currentUpdatesTable.setEnabled(false); + currentUpdatesTable.setToolTipText(null); if (getRowCount() > 0) { int selectThis = engine.getChoiceOfPathStep(oldStep); diff --git a/prism/src/userinterface/simulator/GUISimulatorUpdatesTable.java b/prism/src/userinterface/simulator/GUISimulatorUpdatesTable.java index c97e304d..7866853f 100644 --- a/prism/src/userinterface/simulator/GUISimulatorUpdatesTable.java +++ b/prism/src/userinterface/simulator/GUISimulatorUpdatesTable.java @@ -203,12 +203,11 @@ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionLis class UpdateHeaderRenderer extends JButton implements ListCellRenderer { - boolean selected; ImageIcon selectedIcon; + ImageIcon selectedDisabledIcon; UpdateHeaderRenderer(JTable table) { - selected = false; /*JTableHeader header = table.getTableHeader(); setOpaque(true); setBorder(UIManager.getBorder("TableHeader.cellBorder")); @@ -218,20 +217,20 @@ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionLis setFont(header.getFont());*/ setBorder(null); selectedIcon = GUIPrism.getIconFromImage("smallItemSelected.png"); + selectedDisabledIcon = GUIPrism.getIconFromImage("smallItemSelectedDisabled.png"); } public Component getListCellRendererComponent(JList list, Object value, int index, boolean isSelected, boolean cellHasFocus) { - setBorder(null); - selected = getSelectedRow() == index; - - if (selected) { - setIcon(selectedIcon); + if (getSelectedRow() == index) { + if (GUISimulatorUpdatesTable.this.isEnabled()) + setIcon(selectedIcon); + else + setIcon(selectedDisabledIcon); } else { setIcon(null); } - return this; }