Browse Source
Added a multi-headered table in the simulator. Added this in a general way in userinterface.util.GUIGroupedTable
Added a multi-headered table in the simulator. Added this in a general way in userinterface.util.GUIGroupedTable
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@164 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Mark Kattenbelt
20 years ago
6 changed files with 631 additions and 10 deletions
-
122prism/src/userinterface/simulator/GUISimulator.java
-
15prism/src/userinterface/simulator/GUISimulatorPathTable.java
-
118prism/src/userinterface/util/GUIGroupedTable.java
-
145prism/src/userinterface/util/GUIGroupedTableColumnModel.java
-
188prism/src/userinterface/util/GUIGroupedTableHeader.java
-
53prism/src/userinterface/util/GUIGroupedTableModel.java
@ -0,0 +1,118 @@ |
|||||
|
//============================================================================== |
||||
|
// |
||||
|
// Copyright (c) 2002-2006, Mark Kattenbelt |
||||
|
// |
||||
|
// This file is part of PRISM. |
||||
|
// |
||||
|
// PRISM is free software; you can redistribute it and/or modify |
||||
|
// it under the terms of the GNU General Public License as published by |
||||
|
// the Free Software Foundation; either version 2 of the License, or |
||||
|
// (at your option) any later version. |
||||
|
// |
||||
|
// PRISM is distributed in the hope that it will be useful, |
||||
|
// but WITHOUT ANY WARRANTY; without even the implied warranty of |
||||
|
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
||||
|
// GNU General Public License for more details. |
||||
|
// |
||||
|
// You should have received a copy of the GNU General Public License |
||||
|
// along with PRISM; if not, write to the Free Software Foundation, |
||||
|
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA |
||||
|
// |
||||
|
//============================================================================== |
||||
|
|
||||
|
package userinterface.util; |
||||
|
|
||||
|
import javax.swing.*; |
||||
|
import javax.swing.table.*; |
||||
|
|
||||
|
import java.util.*; |
||||
|
|
||||
|
|
||||
|
/** |
||||
|
* @author mxk |
||||
|
* A table object that is capable of grouping headers, effectively by means of two JTableHeader |
||||
|
* Objects on top of each other. |
||||
|
*/ |
||||
|
public class GUIGroupedTable extends JTable |
||||
|
{ |
||||
|
|
||||
|
/** |
||||
|
* Creates a new GUIGroupedTable. |
||||
|
* @param tableModel The (grouped) table data model on which to base this table. |
||||
|
*/ |
||||
|
public GUIGroupedTable(GUIGroupedTableModel tableModel) |
||||
|
{ |
||||
|
super(tableModel); |
||||
|
} |
||||
|
|
||||
|
/** |
||||
|
* The default TableColumnModel Object (and the only valid one) is a GUIGroupedColumnModel Object. |
||||
|
* @see javax.swing.JTable#createDefaultColumnModel() |
||||
|
*/ |
||||
|
@Override |
||||
|
protected TableColumnModel createDefaultColumnModel() |
||||
|
{ |
||||
|
return new GUIGroupedTableColumnModel(); |
||||
|
} |
||||
|
|
||||
|
|
||||
|
/** |
||||
|
* Given a GUIGroupedTableModel, this function creates a GUIGroupedColumnModel. |
||||
|
* This function is called by JTable when the structure of the table changes, such that |
||||
|
* it is not necessary to worry about the header. |
||||
|
* @see javax.swing.JTable#createDefaultColumnsFromModel() |
||||
|
*/ |
||||
|
@Override |
||||
|
public void createDefaultColumnsFromModel() |
||||
|
{ |
||||
|
GUIGroupedTableColumnModel groupedColumnModel = (GUIGroupedTableColumnModel)columnModel; |
||||
|
|
||||
|
groupedColumnModel.clear(); |
||||
|
|
||||
|
if (dataModel != null && dataModel instanceof GUIGroupedTableModel && columnModel instanceof GUIGroupedTableColumnModel) |
||||
|
{ |
||||
|
GUIGroupedTableModel groupedDataModel = (GUIGroupedTableModel)dataModel; |
||||
|
|
||||
|
int group = 0; |
||||
|
int element = 0; |
||||
|
|
||||
|
// Add a group every iteration |
||||
|
while (group < groupedDataModel.getGroupCount() && element < groupedDataModel.getColumnCount()) |
||||
|
{ |
||||
|
ArrayList groupElements = new ArrayList(); |
||||
|
|
||||
|
// Add an element every iteration |
||||
|
while (groupedDataModel.getLastColumnOfGroup(group) >= element) |
||||
|
{ |
||||
|
TableColumn elementColumn = new TableColumn(element); |
||||
|
elementColumn.setHeaderValue(groupedDataModel.getColumnName(element)); |
||||
|
groupElements.add(elementColumn); |
||||
|
element++; |
||||
|
} |
||||
|
|
||||
|
TableColumn groupColumn = new TableColumn(group); |
||||
|
groupColumn.setHeaderValue(groupedDataModel.getGroupName(group)); |
||||
|
group++; |
||||
|
|
||||
|
groupedColumnModel.addColumnGroup(groupColumn, groupElements); |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
/** |
||||
|
* Creates a default table header from the current column model. |
||||
|
* Also called by JTable such that there is no need to worry about headers once you implemented |
||||
|
* GUIGroupedTableModel. |
||||
|
* @see javax.swing.JTable#createDefaultTableHeader() |
||||
|
*/ |
||||
|
@Override |
||||
|
protected JTableHeader createDefaultTableHeader() { |
||||
|
|
||||
|
if (columnModel != null && columnModel instanceof GUIGroupedTableColumnModel) |
||||
|
{ |
||||
|
return new GUIGroupedTableHeader((GUIGroupedTableColumnModel)columnModel); |
||||
|
} |
||||
|
return new GUIGroupedTableHeader(new GUIGroupedTableColumnModel()); |
||||
|
} |
||||
|
} |
||||
|
|
||||
@ -0,0 +1,145 @@ |
|||||
|
//============================================================================== |
||||
|
// |
||||
|
// Copyright (c) 2002-2006, Mark Kattenbelt |
||||
|
// |
||||
|
// This file is part of PRISM. |
||||
|
// |
||||
|
// PRISM is free software; you can redistribute it and/or modify |
||||
|
// it under the terms of the GNU General Public License as published by |
||||
|
// the Free Software Foundation; either version 2 of the License, or |
||||
|
// (at your option) any later version. |
||||
|
// |
||||
|
// PRISM is distributed in the hope that it will be useful, |
||||
|
// but WITHOUT ANY WARRANTY; without even the implied warranty of |
||||
|
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
||||
|
// GNU General Public License for more details. |
||||
|
// |
||||
|
// You should have received a copy of the GNU General Public License |
||||
|
// along with PRISM; if not, write to the Free Software Foundation, |
||||
|
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA |
||||
|
// |
||||
|
//============================================================================== |
||||
|
|
||||
|
package userinterface.util; |
||||
|
|
||||
|
import java.util.*; |
||||
|
import javax.swing.event.*; |
||||
|
import javax.swing.table.*; |
||||
|
|
||||
|
/** |
||||
|
* @author mxk |
||||
|
* The TableColumnModel with the addition of Groups. A group is a set of columns. The set of columns |
||||
|
* belonging to each group are disjoint and non-empty (!). |
||||
|
*/ |
||||
|
/** |
||||
|
* @author mxk |
||||
|
* |
||||
|
*/ |
||||
|
public class GUIGroupedTableColumnModel extends DefaultTableColumnModel implements TableColumnModelListener |
||||
|
{ |
||||
|
//private DefaultTableColumnModel elementTableColumnModel; |
||||
|
private DefaultTableColumnModel groupTableColumnModel; |
||||
|
|
||||
|
// The nth element is the index of the last element in the nth group. |
||||
|
private ArrayList lastColumn; |
||||
|
|
||||
|
/** |
||||
|
* Creates a new GUIGroupedTableModel with no groups. |
||||
|
*/ |
||||
|
public GUIGroupedTableColumnModel() |
||||
|
{ |
||||
|
lastColumn = new ArrayList(); |
||||
|
|
||||
|
//this.elementTableColumnModel = new DefaultTableColumnModel(); |
||||
|
this.groupTableColumnModel = new DefaultTableColumnModel(); |
||||
|
} |
||||
|
|
||||
|
|
||||
|
/** |
||||
|
* Returns The columns of all groups in terms of a DefaultTableColumnModel. |
||||
|
* @return The columns of all groups in terms of a DefaultTableColumnModel. |
||||
|
*/ |
||||
|
public DefaultTableColumnModel getGroupTableColumnModel() |
||||
|
{ |
||||
|
return groupTableColumnModel; |
||||
|
} |
||||
|
|
||||
|
|
||||
|
/** |
||||
|
* Adds a group to this grouped column model. |
||||
|
* @param groupColumn A TableColumn representing all of the group. |
||||
|
* @param elementColumns An ArrayList of TableColumns representing the columns of this group in the model. |
||||
|
*/ |
||||
|
public void addColumnGroup(TableColumn groupColumn, ArrayList elementColumns) |
||||
|
{ |
||||
|
groupTableColumnModel.addColumn(groupColumn); |
||||
|
|
||||
|
for (int i = 0; i < elementColumns.size(); i++) |
||||
|
{ |
||||
|
this.addColumn(((TableColumn)elementColumns.get(i))); |
||||
|
} |
||||
|
|
||||
|
lastColumn.add(new Integer(this.getColumnCount()-1)); |
||||
|
} |
||||
|
|
||||
|
/** |
||||
|
* A function that updates the widths of the group columns. |
||||
|
*/ |
||||
|
public void updateGroups() |
||||
|
{ |
||||
|
int group = 0; |
||||
|
int groupWidth = 0; |
||||
|
|
||||
|
for (int i = 0; i < this.getColumnCount(); i++) |
||||
|
{ |
||||
|
groupWidth += this.getColumn(i).getWidth(); |
||||
|
|
||||
|
// If this is the last column of a group. |
||||
|
if (i == ((Integer)lastColumn.get(group)).intValue()) |
||||
|
{ |
||||
|
while (group < groupTableColumnModel.getColumnCount() && i == ((Integer)lastColumn.get(group)).intValue()) |
||||
|
{ |
||||
|
groupTableColumnModel.getColumn(group).setWidth(groupWidth); |
||||
|
|
||||
|
groupWidth = 0; |
||||
|
group++; |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
public void columnAdded(TableColumnModelEvent e) {} |
||||
|
public void columnMarginChanged(ChangeEvent e) {} |
||||
|
public void columnMoved(TableColumnModelEvent e) {} |
||||
|
public void columnRemoved(TableColumnModelEvent e) {} |
||||
|
public void columnSelectionChanged(ListSelectionEvent e) {} |
||||
|
|
||||
|
/** |
||||
|
* If something changed in the columns of the table, then adjust the group widths. |
||||
|
*/ |
||||
|
@Override |
||||
|
protected void fireColumnMarginChanged() { |
||||
|
// Size must have changed then. |
||||
|
updateGroups(); |
||||
|
super.fireColumnMarginChanged(); |
||||
|
} |
||||
|
|
||||
|
/** |
||||
|
* Empties this GUIGroupedTableColumnModel. |
||||
|
*/ |
||||
|
public void clear() |
||||
|
{ |
||||
|
while (this.getColumnCount() > 0) |
||||
|
{ |
||||
|
this.removeColumn(this.getColumn(0)); |
||||
|
} |
||||
|
|
||||
|
while (groupTableColumnModel.getColumnCount() > 0) |
||||
|
{ |
||||
|
groupTableColumnModel.removeColumn(groupTableColumnModel.getColumn(0)); |
||||
|
} |
||||
|
|
||||
|
this.lastColumn.clear(); |
||||
|
} |
||||
|
} |
||||
|
|
||||
@ -0,0 +1,188 @@ |
|||||
|
//============================================================================== |
||||
|
// |
||||
|
// Copyright (c) 2002-2006, Mark Kattenbelt |
||||
|
// |
||||
|
// This file is part of PRISM. |
||||
|
// |
||||
|
// PRISM is free software; you can redistribute it and/or modify |
||||
|
// it under the terms of the GNU General Public License as published by |
||||
|
// the Free Software Foundation; either version 2 of the License, or |
||||
|
// (at your option) any later version. |
||||
|
// |
||||
|
// PRISM is distributed in the hope that it will be useful, |
||||
|
// but WITHOUT ANY WARRANTY; without even the implied warranty of |
||||
|
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
||||
|
// GNU General Public License for more details. |
||||
|
// |
||||
|
// You should have received a copy of the GNU General Public License |
||||
|
// along with PRISM; if not, write to the Free Software Foundation, |
||||
|
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA |
||||
|
// |
||||
|
//============================================================================== |
||||
|
|
||||
|
package userinterface.util; |
||||
|
|
||||
|
import java.awt.*; |
||||
|
import java.awt.event.*; |
||||
|
|
||||
|
import javax.swing.*; |
||||
|
import javax.swing.event.*; |
||||
|
import javax.swing.table.*; |
||||
|
|
||||
|
|
||||
|
/** |
||||
|
* @author mxk |
||||
|
* An object to represent a grouped TableHeader. It extends JTableHeader, but actually consists of two separate |
||||
|
* JTableHeaders. Some of this could be tidied up, but it is build more or less to Swings concepts. |
||||
|
*/ |
||||
|
public class GUIGroupedTableHeader extends JTableHeader implements TableColumnModelListener, MouseListener |
||||
|
{ |
||||
|
private JTableHeader bottomHeader; |
||||
|
private JTableHeader topHeader; |
||||
|
|
||||
|
/** |
||||
|
* Creates a new GUIGroupedTableHeader. |
||||
|
* @param model The column model that is the basis of this table header (must be grouped). |
||||
|
*/ |
||||
|
public GUIGroupedTableHeader(GUIGroupedTableColumnModel model) |
||||
|
{ |
||||
|
super(); |
||||
|
removeAll(); |
||||
|
|
||||
|
topHeader = new JTableHeader(model.getGroupTableColumnModel()); |
||||
|
topHeader.setResizingAllowed(false); |
||||
|
topHeader.setReorderingAllowed(false); |
||||
|
|
||||
|
final TableCellRenderer renderer = topHeader.getDefaultRenderer(); |
||||
|
topHeader.setDefaultRenderer(new TableCellRenderer() { |
||||
|
public Component getTableCellRendererComponent(JTable table, Object value, boolean isSelected, boolean hasFocus, int row, int column) |
||||
|
{ |
||||
|
Component component = renderer.getTableCellRendererComponent(table, value, isSelected, hasFocus, row, column); |
||||
|
component.setFont(topHeader.getFont().deriveFont(Font.BOLD)); |
||||
|
return component; |
||||
|
} |
||||
|
}); |
||||
|
|
||||
|
bottomHeader = new JTableHeader(model); |
||||
|
bottomHeader.setReorderingAllowed(false); |
||||
|
|
||||
|
setLayout(new GridLayout(2,1)); |
||||
|
|
||||
|
add(topHeader); |
||||
|
add(bottomHeader); |
||||
|
|
||||
|
model.updateGroups(); |
||||
|
|
||||
|
this.setPreferredSize(new Dimension(bottomHeader.getPreferredSize().width, bottomHeader.getPreferredSize().height * 2)); |
||||
|
this.setMinimumSize(new Dimension(bottomHeader.getMinimumSize().width, bottomHeader.getMinimumSize().height * 2)); |
||||
|
this.setMaximumSize(new Dimension(bottomHeader.getMaximumSize().width, bottomHeader.getMaximumSize().height * 2)); |
||||
|
|
||||
|
Component[] cs = this.getComponents(); |
||||
|
for (int i = 0; i < cs.length; i++) |
||||
|
{ |
||||
|
cs[i].addMouseListener(this); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
|
||||
|
/** |
||||
|
* A fairly ugly hack to prevent a CellRenderer to be added to this container. More elegant solutions are welcome. |
||||
|
* @see java.awt.Container#addImpl(java.awt.Component, java.lang.Object, int) |
||||
|
*/ |
||||
|
@Override |
||||
|
protected void addImpl(Component comp, Object constraints, int index) { |
||||
|
// TODO Auto-generated method stub |
||||
|
if (this.getComponents().length < 2) |
||||
|
{ |
||||
|
super.addImpl(comp, constraints, index); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
/** |
||||
|
* Overwritten to never allow reordering. |
||||
|
* @see javax.swing.table.JTableHeader#setReorderingAllowed(boolean) |
||||
|
*/ |
||||
|
@Override |
||||
|
public void setReorderingAllowed(boolean reorderingAllowed) { |
||||
|
super.setReorderingAllowed(false); |
||||
|
} |
||||
|
|
||||
|
/** |
||||
|
* Overwritten to always return the resizing column of the bottom JTableHeader. |
||||
|
* @see javax.swing.table.JTableHeader#getResizingColumn() |
||||
|
*/ |
||||
|
@Override |
||||
|
public TableColumn getResizingColumn() |
||||
|
{ |
||||
|
return bottomHeader.getResizingColumn(); |
||||
|
} |
||||
|
|
||||
|
/** |
||||
|
* Overwritten to give the JTableHeaders a change to resize as well. |
||||
|
* @see javax.swing.table.JTableHeader#resizeAndRepaint() |
||||
|
*/ |
||||
|
@Override |
||||
|
public void resizeAndRepaint() |
||||
|
{ |
||||
|
if (topHeader != null && bottomHeader != null) |
||||
|
{ |
||||
|
this.setPreferredSize(new Dimension(bottomHeader.getPreferredSize().width, bottomHeader.getPreferredSize().height * 2)); |
||||
|
this.setMinimumSize(new Dimension(bottomHeader.getMinimumSize().width, bottomHeader.getMinimumSize().height * 2)); |
||||
|
this.setMaximumSize(new Dimension(bottomHeader.getMaximumSize().width, bottomHeader.getMaximumSize().height * 2)); |
||||
|
|
||||
|
this.doLayout(); |
||||
|
} |
||||
|
|
||||
|
super.resizeAndRepaint(); |
||||
|
} |
||||
|
|
||||
|
/** |
||||
|
* Set the column model. |
||||
|
* @param columnModel The grouped column model to use. |
||||
|
*/ |
||||
|
public void setColumnModel(GUIGroupedTableColumnModel columnModel) { |
||||
|
|
||||
|
topHeader.setColumnModel(columnModel.getGroupTableColumnModel()); |
||||
|
bottomHeader.setColumnModel(columnModel); |
||||
|
|
||||
|
this.resizeAndRepaint(); |
||||
|
|
||||
|
columnModel.updateGroups(); |
||||
|
super.setColumnModel(columnModel); |
||||
|
} |
||||
|
|
||||
|
/** |
||||
|
* Overwritten to catch events of child components. |
||||
|
*/ |
||||
|
public void mouseClicked(MouseEvent e) { |
||||
|
this.dispatchEvent(new MouseEvent(this, e.getID(), e.getWhen(), e.getModifiers(), e.getX(), e.getY() + ((Component)e.getSource()).getBounds().y, e.getClickCount(), e.isPopupTrigger())); |
||||
|
} |
||||
|
|
||||
|
/** |
||||
|
* Overwritten to catch events of child components. |
||||
|
*/ |
||||
|
public void mouseEntered(MouseEvent e) { |
||||
|
this.dispatchEvent(new MouseEvent(this, e.getID(), e.getWhen(), e.getModifiers(), e.getX(), e.getY() + ((Component)e.getSource()).getBounds().y, e.getClickCount(), e.isPopupTrigger())); |
||||
|
} |
||||
|
|
||||
|
/** |
||||
|
* Overwritten to catch events of child components. |
||||
|
*/ |
||||
|
public void mouseExited(MouseEvent e) { |
||||
|
this.dispatchEvent(new MouseEvent(this, e.getID(), e.getWhen(), e.getModifiers(), e.getX(), e.getY() + ((Component)e.getSource()).getBounds().y, e.getClickCount(), e.isPopupTrigger())); |
||||
|
} |
||||
|
|
||||
|
/** |
||||
|
* Overwritten to catch events of child components. |
||||
|
*/ |
||||
|
public void mousePressed(MouseEvent e) { |
||||
|
this.dispatchEvent(new MouseEvent(this, e.getID(), e.getWhen(), e.getModifiers(), e.getX(), e.getY() + ((Component)e.getSource()).getBounds().y, e.getClickCount(), e.isPopupTrigger())); |
||||
|
} |
||||
|
|
||||
|
/** |
||||
|
* Overwritten to catch events of child components. |
||||
|
*/ |
||||
|
public void mouseReleased(MouseEvent e) { |
||||
|
this.dispatchEvent(new MouseEvent(this, e.getID(), e.getWhen(), e.getModifiers(), e.getX(), e.getY() + ((Component)e.getSource()).getBounds().y, e.getClickCount(), e.isPopupTrigger())); |
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,53 @@ |
|||||
|
//============================================================================== |
||||
|
// |
||||
|
// Copyright (c) 2002-2006, Mark Kattenbelt |
||||
|
// |
||||
|
// This file is part of PRISM. |
||||
|
// |
||||
|
// PRISM is free software; you can redistribute it and/or modify |
||||
|
// it under the terms of the GNU General Public License as published by |
||||
|
// the Free Software Foundation; either version 2 of the License, or |
||||
|
// (at your option) any later version. |
||||
|
// |
||||
|
// PRISM is distributed in the hope that it will be useful, |
||||
|
// but WITHOUT ANY WARRANTY; without even the implied warranty of |
||||
|
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
||||
|
// GNU General Public License for more details. |
||||
|
// |
||||
|
// You should have received a copy of the GNU General Public License |
||||
|
// along with PRISM; if not, write to the Free Software Foundation, |
||||
|
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA |
||||
|
// |
||||
|
//============================================================================== |
||||
|
|
||||
|
package userinterface.util; |
||||
|
|
||||
|
import javax.swing.table.TableModel; |
||||
|
|
||||
|
/** |
||||
|
* @author mxk |
||||
|
* An interface which extends {@link TableModel} such that also group information can |
||||
|
* be extracted automatically. Note that groups are always non-empty. |
||||
|
*/ |
||||
|
public interface GUIGroupedTableModel extends TableModel |
||||
|
{ |
||||
|
/** |
||||
|
* @return The number of groups in this model. |
||||
|
*/ |
||||
|
public int getGroupCount(); |
||||
|
|
||||
|
/** |
||||
|
* Retrieves the name of a group. |
||||
|
* @param groupIndex The index of a group. |
||||
|
* @return The name of the nth group, where n = groupIndex. |
||||
|
* @see TableModel.getColumnName(int columnIndex). |
||||
|
*/ |
||||
|
public String getGroupName(int groupIndex); |
||||
|
|
||||
|
/** |
||||
|
* Retrieves the index of the last `normal' column in a group. |
||||
|
* @param groupIndex The index of a group. |
||||
|
* @return The index of the last column in this group. |
||||
|
*/ |
||||
|
public int getLastColumnOfGroup(int groupIndex); |
||||
|
} |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue