diff --git a/prism/images/smallItemSelectedDisabled.png b/prism/images/smallItemSelectedDisabled.png new file mode 100644 index 00000000..70f5367e Binary files /dev/null and b/prism/images/smallItemSelectedDisabled.png differ 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; }