s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Fixed bug where the columns could not be hidden (of transitions in the simulator). Also added the feature that the popup menu also reacts on the table header and the surrounding JPanel. If this is the case backtracking is disabled. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@120 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Mark Kattenbelt 19 years ago
parent
df052b0d54
commit
d9993ade2c
1 changed files with 74 additions and 69 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 143
      prism/src/userinterface/simulator/GUISimulator.java

143
prism/src/userinterface/simulator/GUISimulator.java
View File

@ -103,6 +103,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
pathTable.getSelectionModel().addListSelectionListener(this);
pathTable.addMouseListener(this);
pathTable.getTableHeader().addMouseListener(this);
pathTable.getParent().addMouseListener(this);
pathTable.getTableHeader().setReorderingAllowed(false);
@ -1938,7 +1940,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
error(ex.getMessage());
}
}
};
};
removeToHere.putValue(Action.LONG_DESCRIPTION, "Removes states preceding the selected state from the path.");
removeToHere.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_R));
removeToHere.putValue(Action.NAME, "Remove preceding steps");
@ -2065,93 +2067,55 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
{
if(!computing)
{
if(e.isPopupTrigger() && e.getSource() == pathTable)
if(e.isPopupTrigger() && (e.getSource() == pathTable || e.getSource() == pathTable.getTableHeader() || e.getSource() == pathTable.getParent()))
{
int index = pathTable.rowAtPoint(e.getPoint());
backtrackToHere.setEnabled(!(e.getSource() == pathTable.getTableHeader() || e.getSource() == pathTable.getParent()));
removeToHere.setEnabled(!(e.getSource() == pathTable.getTableHeader() || e.getSource() == pathTable.getParent()));
pathTable.getSelectionModel().setSelectionInterval(index, index);
int index = pathTable.rowAtPoint(e.getPoint());
pathTable.getSelectionModel().setSelectionInterval(index, index);
showColumnMenu.removeAll();
//Now populate showColumnMenu with all columns
for(int i = 0; i < pathTableModel.getColumnCount(); i++)
for(int i = 1; i < pathTableModel.getColumnCount(); i++)
{
if(pathTableModel.getColumnName(i).equals("Step")) continue;
JCheckBox showColumn = new JCheckBox(pathTableModel.getColumnName(i));
int colIndex = pathTable.convertColumnIndexToView(i);
// Better to use JCheckBoxMenuItems rather than JCheckBox.
JCheckBoxMenuItem showColumn = new JCheckBoxMenuItem(pathTableModel.getColumnName(i));
// A column is selected if it is present in the view.
showColumn.setSelected(pathTable.convertColumnIndexToView(i) != -1);
showColumn.setSelected(colIndex >= 0);
showColumn.addActionListener(new ActionListener()
showColumn.addItemListener(new ItemListener()
{
public void actionPerformed(ActionEvent e)
public void itemStateChanged(ItemEvent e)
{
JCheckBox check = (JCheckBox)e.getSource();
String text = check.getText();
JCheckBoxMenuItem showColumn = (JCheckBoxMenuItem)e.getSource();
if(check.isSelected())
if (e.getStateChange() == ItemEvent.DESELECTED)
{
TableColumn tc = pathTable.getColumn(showColumn.getText());
hiddenColumns.add(tc);
pathTable.removeColumn(tc);
}
else if (e.getStateChange() == ItemEvent.SELECTED)
{
//search for this in hiddenColumns
//search for this in hiddenColumns
TableColumn tc = null;
for(int i = 0; i < hiddenColumns.size(); i++)
for (int i = 0; i < hiddenColumns.size(); i++)
{
tc = (TableColumn)hiddenColumns.get(i);
if(tc.getHeaderValue().equals(text))
if(tc.getHeaderValue().equals(showColumn.getText()))
break;
}
if(tc == null) return;
hiddenColumns.remove(tc);
pathTable.addColumn(tc);
}
else
{
TableColumn tc = pathTable.getColumn(text);
hiddenColumns.add(tc);
pathTable.removeColumn(tc);
insertTableColumn(tc);
hiddenColumns.remove(tc);
}
sortOutColumnSizes();
}
});
/*showColumn.addMouseListener(new MouseListener()
{
public void mouseClicked(MouseEvent e)
{
}
public void mouseReleased(MouseEvent e)
{
}
public void mousePressed(MouseEvent e)
{
}
public void mouseEntered(MouseEvent e)
{
JCheckBox check = (JCheckBox)e.getSource();
check.setBackground(Color.CYAN);
}
public void mouseExited(MouseEvent e)
{
JCheckBox check = (JCheckBox)e.getSource();
check.setBackground(Color.lightGray);
}
});*/
});
showColumnMenu.add(showColumn);
}
@ -2165,8 +2129,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
{
for(int i = hiddenColumns.size()-1; i>=0; i--)
{
TableColumn tc = (TableColumn)hiddenColumns.get(i);
pathTable.addColumn(tc);
TableColumn tc = (TableColumn) hiddenColumns.get(i);
insertTableColumn(tc);
hiddenColumns.remove(tc);
}
@ -2182,6 +2146,47 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
}
}
public void insertTableColumn(TableColumn column)
{
int i = 1;
int j = 1;
String text = (String) column.getHeaderValue();
while (j <= pathTable.getColumnCount() && i < pathTableModel.getColumnCount())
{
if (j == pathTable.getColumnCount())
{
// Found the location
pathTable.addColumn(column);
break;
}
else
{
String tcj = pathTable.getColumnName(j);
String tci = pathTableModel.getColumnName(i);
if (tci.equals(text))
{
// Found the location
pathTable.addColumn(column);
// Move to location
if (j != pathTable.getColumnCount()-1)
pathTable.moveColumn(pathTable.getColumnCount()-1, j);
break;
}
else
{
i++;
if (tci.equals(tcj)) { j++; }
}
}
}
}
public void showColumn(int i )
{

Write Preview
Loading…
Cancel
Save