From a5cd6a4b5647071b47a6f4a033fefec6777b9c25 Mon Sep 17 00:00:00 2001 From: Mark Kattenbelt Date: Fri, 19 Oct 2007 18:27:31 +0000 Subject: [PATCH] Fixed bug where java 1.6 gave an exception when clicking on path table header. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@469 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/userinterface/util/GUIGroupedTable.java | 15 +++++++++++---- .../userinterface/util/GUIGroupedTableHeader.java | 14 +++++++++----- 2 files changed, 20 insertions(+), 9 deletions(-) diff --git a/prism/src/userinterface/util/GUIGroupedTable.java b/prism/src/userinterface/util/GUIGroupedTable.java index 2fdda2ce..40e490f3 100644 --- a/prism/src/userinterface/util/GUIGroupedTable.java +++ b/prism/src/userinterface/util/GUIGroupedTable.java @@ -112,11 +112,18 @@ public class GUIGroupedTable extends JTable @Override protected JTableHeader createDefaultTableHeader() { + GUIGroupedTableHeader header = null; + if (columnModel != null && columnModel instanceof GUIGroupedTableColumnModel) - { - return new GUIGroupedTableHeader((GUIGroupedTableColumnModel)columnModel, (GUIGroupedTableModel)this.getModel()); - } - return new GUIGroupedTableHeader(new GUIGroupedTableColumnModel(), (GUIGroupedTableModel)this.getModel()); + header = new GUIGroupedTableHeader((GUIGroupedTableColumnModel)columnModel, (GUIGroupedTableModel)this.getModel(), this); + else + header = new GUIGroupedTableHeader(new GUIGroupedTableColumnModel(), (GUIGroupedTableModel)this.getModel(), this); + + header.setTable(this); + + return header; } } + + diff --git a/prism/src/userinterface/util/GUIGroupedTableHeader.java b/prism/src/userinterface/util/GUIGroupedTableHeader.java index 7c47717c..891c68cc 100644 --- a/prism/src/userinterface/util/GUIGroupedTableHeader.java +++ b/prism/src/userinterface/util/GUIGroupedTableHeader.java @@ -50,19 +50,20 @@ public class GUIGroupedTableHeader extends JTableHeader implements TableColumnMo * Creates a new GUIGroupedTableHeader. * @param model The column model that is the basis of this table header (must be grouped). */ - public GUIGroupedTableHeader(GUIGroupedTableColumnModel model, GUIGroupedTableModel tableModel) + public GUIGroupedTableHeader(GUIGroupedTableColumnModel model, GUIGroupedTableModel tableModel, GUIGroupedTable table) { super(); removeAll(); this.model = model; this.tableModel = tableModel; - + 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) @@ -75,7 +76,10 @@ public class GUIGroupedTableHeader extends JTableHeader implements TableColumnMo bottomHeader = new JTableHeader(model); bottomHeader.setReorderingAllowed(false); - + + topHeader.setTable(table); + bottomHeader.setTable(table); + setLayout(new GridLayout(2,1)); add(topHeader); @@ -119,7 +123,7 @@ public class GUIGroupedTableHeader extends JTableHeader implements TableColumnMo }); bottomHeader.addMouseMotionListener(new MouseMotionAdapter() { -private TableColumn lastColumn; + private TableColumn lastColumn; public void mouseMoved(MouseEvent e) { @@ -217,7 +221,7 @@ private TableColumn lastColumn; * 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())); + this.dispatchEvent(new MouseEvent(this, e.getID(), e.getWhen(), e.getModifiers(), e.getX(), e.getY() + ((Component)e.getSource()).getBounds().y, e.getClickCount(), e.isPopupTrigger())); } /**