diff --git a/prism/src/settings/SettingTable.java b/prism/src/settings/SettingTable.java index e5862d3a..dbabcd80 100644 --- a/prism/src/settings/SettingTable.java +++ b/prism/src/settings/SettingTable.java @@ -3,6 +3,7 @@ // Copyright (c) 2002- // Authors: // * Andrew Hinton (University of Birmingham) +// * Dave Parker (University of Birmingham) // //------------------------------------------------------------------------------ // @@ -310,6 +311,13 @@ public class SettingTable extends JPanel implements ListSelectionListener, Table }//GEN-END:initComponents + /** Override set font to update row heights at same time */ + public void setFont(Font font) + { + super.setFont(font); + if (theTable != null) theTable.setRowHeight(getFontMetrics(font).getHeight()+4); + } + public void valueChanged(ListSelectionEvent e) { //System.out.println("list VALUE CHANGED"); diff --git a/prism/src/userinterface/GUIConstantsPicker.java b/prism/src/userinterface/GUIConstantsPicker.java index 7bf70aa2..73691ec9 100644 --- a/prism/src/userinterface/GUIConstantsPicker.java +++ b/prism/src/userinterface/GUIConstantsPicker.java @@ -86,6 +86,8 @@ public class GUIConstantsPicker extends javax.swing.JDialog modelTable.setSelectionMode(DefaultListSelectionModel.SINGLE_INTERVAL_SELECTION); propTable.setCellSelectionEnabled(true); modelTable.setCellSelectionEnabled(true); + propTable.setRowHeight(getFontMetrics(propTable.getFont()).getHeight() + 4); + modelTable.setRowHeight(getFontMetrics(modelTable.getFont()).getHeight() + 4); //initialise initComponents(); diff --git a/prism/src/userinterface/GUIPrism.java b/prism/src/userinterface/GUIPrism.java index 298f6ebb..d662db85 100644 --- a/prism/src/userinterface/GUIPrism.java +++ b/prism/src/userinterface/GUIPrism.java @@ -378,6 +378,8 @@ public class GUIPrism extends JFrame } } SwingUtilities.updateComponentTreeUI(this); + SwingUtilities.updateComponentTreeUI(choose); + SwingUtilities.updateComponentTreeUI(options); repaint(); } diff --git a/prism/src/userinterface/properties/ConstantHeader.java b/prism/src/userinterface/properties/ConstantHeader.java index 6c016454..8b123c98 100644 --- a/prism/src/userinterface/properties/ConstantHeader.java +++ b/prism/src/userinterface/properties/ConstantHeader.java @@ -27,6 +27,9 @@ package userinterface.properties; +import javax.swing.*; +import java.awt.*; + /** * * @author ug60axh @@ -37,7 +40,8 @@ public class ConstantHeader extends javax.swing.JPanel /** Creates new form ConstantLine */ public ConstantHeader() { - initComponents(); + initComponents(); + setPreferredSize(new Dimension(1, 2*(getFontMetrics(getFont()).getHeight() + 4))); } /** This method is called from within the constructor to diff --git a/prism/src/userinterface/properties/ConstantLine.java b/prism/src/userinterface/properties/ConstantLine.java index a87d3181..efceca95 100644 --- a/prism/src/userinterface/properties/ConstantLine.java +++ b/prism/src/userinterface/properties/ConstantLine.java @@ -49,6 +49,7 @@ public class ConstantLine extends javax.swing.JPanel { initComponents(); setBorder(new BottomBorder()); + setPreferredSize(new Dimension(1, getFontMetrics(getFont()).getHeight() + 4)); setConstName(name); setConstType(type); doDefaults(); diff --git a/prism/src/userinterface/properties/GUIExperimentTable.java b/prism/src/userinterface/properties/GUIExperimentTable.java index 914b0e33..9ab46162 100644 --- a/prism/src/userinterface/properties/GUIExperimentTable.java +++ b/prism/src/userinterface/properties/GUIExperimentTable.java @@ -55,6 +55,13 @@ public class GUIExperimentTable extends JTable col.setCellRenderer(new ProgressBarRenderer()); } + /** Override set font to update row heights at same time */ + public void setFont(Font font) + { + super.setFont(font); + setRowHeight(getFontMetrics(font).getHeight() + 4); + } + //UPDATE METHODS public void deleteSelected() diff --git a/prism/src/userinterface/properties/GUIPropConstantList.java b/prism/src/userinterface/properties/GUIPropConstantList.java index fcff321d..31cdcd5e 100644 --- a/prism/src/userinterface/properties/GUIPropConstantList.java +++ b/prism/src/userinterface/properties/GUIPropConstantList.java @@ -51,6 +51,13 @@ public class GUIPropConstantList extends JTable setEditorAndRenderer(); } + /** Override set font to update row heights at same time */ + public void setFont(Font font) + { + super.setFont(font); + setRowHeight(getFontMetrics(font).getHeight() + 4); + } + protected void setEditorAndRenderer() { JComboBox typeChooser = new JComboBox(); diff --git a/prism/src/userinterface/properties/GUIPropLabelList.java b/prism/src/userinterface/properties/GUIPropLabelList.java index dea97055..6fc66547 100644 --- a/prism/src/userinterface/properties/GUIPropLabelList.java +++ b/prism/src/userinterface/properties/GUIPropLabelList.java @@ -51,6 +51,13 @@ public class GUIPropLabelList extends JTable try { setDefaultRenderer(Class.forName("java.lang.Object"), new TheCellRenderer()); } catch (ClassNotFoundException e) {} } + /** Override set font to update row heights at same time */ + public void setFont(Font font) + { + super.setFont(font); + setRowHeight(getFontMetrics(font).getHeight() + 4); + } + public void correctEditors() { if(this.getCellEditor() != null) diff --git a/prism/src/userinterface/properties/GUIPropertiesList.java b/prism/src/userinterface/properties/GUIPropertiesList.java index 84dbd9df..06f4ab20 100644 --- a/prism/src/userinterface/properties/GUIPropertiesList.java +++ b/prism/src/userinterface/properties/GUIPropertiesList.java @@ -73,6 +73,14 @@ public class GUIPropertiesList extends JList implements KeyListener getInputMap().put(KeyStroke.getKeyStroke(KeyEvent.VK_C, InputEvent.CTRL_MASK), "none"); } + /** Override set font to update row heights at same time */ + public void setFont(Font font) + { + super.setFont(font); + // Note: minimum of 20 since icons are 16x16 + if (font != null) setFixedCellHeight(Math.max(20, getFontMetrics(font).getHeight() + 4)); + } + //ACCESS METHODS public int getNumProperties() @@ -382,7 +390,6 @@ public class GUIPropertiesList extends JList implements KeyListener toolTip = p.getToolTipText(); // text - setFont(parent.getListFont()); setText(p.getPropString()); // icon diff --git a/prism/src/userinterface/properties/GUIResultsTable.java b/prism/src/userinterface/properties/GUIResultsTable.java index 678f63f7..eaf632b6 100644 --- a/prism/src/userinterface/properties/GUIResultsTable.java +++ b/prism/src/userinterface/properties/GUIResultsTable.java @@ -62,6 +62,7 @@ public class GUIResultsTable extends javax.swing.JDialog table = new JTable(); table.setModel(tableModel); table.setCellSelectionEnabled(true); + table.setRowHeight(getFontMetrics(table.getFont()).getHeight() + 4); //initialise initComponents(); diff --git a/prism/src/userinterface/properties/GraphConstantHeader.java b/prism/src/userinterface/properties/GraphConstantHeader.java index aca1f578..5b1c1465 100644 --- a/prism/src/userinterface/properties/GraphConstantHeader.java +++ b/prism/src/userinterface/properties/GraphConstantHeader.java @@ -27,6 +27,9 @@ package userinterface.properties; +import javax.swing.*; +import java.awt.*; + /** * * @author ug60axh @@ -37,7 +40,8 @@ public class GraphConstantHeader extends javax.swing.JPanel /** Creates new form ConstantLine */ public GraphConstantHeader() { - initComponents(); + initComponents(); + setPreferredSize(new Dimension(1, getFontMetrics(getFont()).getHeight() + 4)); } public void setEnabled(boolean b) diff --git a/prism/src/userinterface/simulator/GUIInitialStatePicker.java b/prism/src/userinterface/simulator/GUIInitialStatePicker.java index e4a94cc1..f80f2e80 100644 --- a/prism/src/userinterface/simulator/GUIInitialStatePicker.java +++ b/prism/src/userinterface/simulator/GUIInitialStatePicker.java @@ -86,7 +86,8 @@ public class GUIInitialStatePicker extends javax.swing.JDialog implements KeyLis initValuesTable.setModel(initValuesModel); initValuesTable.setSelectionMode(DefaultListSelectionModel.SINGLE_INTERVAL_SELECTION); initValuesTable.setCellSelectionEnabled(true); - + initValuesTable.setRowHeight(getFontMetrics(initValuesTable.getFont()).getHeight() + 4); + this.initialState = defaultInitial; //initialise diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index e13b054b..ff12271e 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -4,6 +4,7 @@ // Authors: // * Andrew Hinton (University of Birmingham) // * Mark Kattenbelt (University of Birmingham) +// * Dave Parker (University of Birmingham) // //------------------------------------------------------------------------------ // @@ -164,7 +165,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect lastInitialState = null; - tableScroll.setRowHeaderView(((GUISimulatorPathTable)pathTable).getPathRowHeader()); + tableScroll.setRowHeaderView(((GUISimulatorPathTable)pathTable).getPathLoopIndicator()); manualUpdateTableScrollPane.setRowHeaderView(((GUISimulatorUpdatesTable)currentUpdatesTable).getUpdateRowHeader()); tableScroll.setHorizontalScrollBarPolicy(JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED); @@ -1454,6 +1455,13 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect }// //GEN-END:initComponents + /** Override set font to set pass on to path table and header (which may not be visible yet) */ + public void setFont(Font font) + { + super.setFont(font); + if (pathTable != null) pathTable.setFont(font); + } + private void inputBacktrackFieldActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_inputBacktrackFieldActionPerformed // TODO add your handling code here: }//GEN-LAST:event_inputBacktrackFieldActionPerformed diff --git a/prism/src/userinterface/simulator/GUISimulatorPathTable.java b/prism/src/userinterface/simulator/GUISimulatorPathTable.java index 985be471..3b7b509f 100644 --- a/prism/src/userinterface/simulator/GUISimulatorPathTable.java +++ b/prism/src/userinterface/simulator/GUISimulatorPathTable.java @@ -4,6 +4,7 @@ // Authors: // * Andrew Hinton (University of Birmingham) // * Mark Kattenbelt (University of Birmingham) +// * Dave Parker (University of Birmingham) // //------------------------------------------------------------------------------ // @@ -43,21 +44,15 @@ import javax.swing.plaf.basic.*; import javax.swing.plaf.*; import javax.swing.event.*; - -/** - * - * @author ug60axh - */ public class GUISimulatorPathTable extends GUIGroupedTable { - private GUISimulator.PathTableModel ptm; - private PathRowHeader pathRowHeader; - private SimulatorEngine engine; private GUISimulator simulator; - - private JList header; - private GUISimulatorPathTable.RowHeaderListModel headerModel; + // Table model + private GUISimulator.PathTableModel ptm; + // Component on left hand side to show path loops + private JList loopIndicator; + private LoopIndicatorListModel loopIndicatorModel; /** Creates a new instance of GUISimulatorPathTable */ public GUISimulatorPathTable(GUISimulator simulator, GUISimulator.PathTableModel ptm, SimulatorEngine engine) @@ -67,30 +62,27 @@ public class GUISimulatorPathTable extends GUIGroupedTable this.simulator = simulator; this.engine = engine; + // Table setColumnSelectionAllowed(false); getSelectionModel().setSelectionMode(ListSelectionModel.SINGLE_SELECTION); - - pathRowHeader = new GUISimulatorPathTable.PathRowHeader(); - - headerModel = new RowHeaderListModel(); - JList rowHeader = new JList(headerModel); - - rowHeader.setBackground(new JPanel().getBackground()); - - rowHeader.setFixedCellWidth(25); - - rowHeader.setFixedCellHeight(getRowHeight()); - //+ getRowMargin()); - //getIntercellSpacing().height); - rowHeader.setCellRenderer(new RowHeaderRenderer(this)); - - this.header = rowHeader; - setDefaultRenderer(Object.class, new PathChangeTableRenderer(true)); - - + // Loop indicator + loopIndicatorModel = new LoopIndicatorListModel(); + loopIndicator = new JList(loopIndicatorModel); + loopIndicator.setBackground(new JPanel().getBackground()); + loopIndicator.setFixedCellWidth(25); + loopIndicator.setFixedCellHeight(getRowHeight()); + loopIndicator.setCellRenderer(new LoopIndicatorRenderer(this)); } + /** Override set font to set row height(s) */ + public void setFont(Font font) + { + super.setFont(font); + setRowHeight(getFontMetrics(font).getHeight() + 4); + if (loopIndicator != null) loopIndicator.setFixedCellHeight(getRowHeight()); + } + public boolean usingChangeRenderer() { return ((PathChangeTableRenderer)getDefaultRenderer(Object.class)).onlyShowChange(); @@ -111,55 +103,21 @@ public class GUISimulatorPathTable extends GUIGroupedTable public void paintComponent(Graphics g) { super.paintComponent(g); - - //pathRowHeader.paintComponent(g); - headerModel.updateHeader(); + loopIndicatorModel.updateIndicator(); } - /** - * Getter for property pathRowHeader. - * @return Value of property pathRowHeader. - */ - public Component getPathRowHeader() + public Component getPathLoopIndicator() { - return header; //pathRowHeader; + return loopIndicator; } - class PathRowHeader extends JPanel - { - public PathRowHeader() - { - super(); - - - setBackground(Color.yellow); - } - - public void paintComponent(Graphics g) - { - super.paintComponent(g); - - Graphics2D g2 = (Graphics2D) g; - - g2.clearRect(0,0,getWidth(), getHeight()); - - g2.setColor(Color.black); - double y; - for(int i = 0; i < ptm.getRowCount(); i++) - { - y = i * 10; - - g2.drawLine(0, (int)y, 10, (int)y); - } - } - } + // Cell renderer for list representing loop indicator (left of path table) - class RowHeaderRenderer extends JPanel implements ListCellRenderer + class LoopIndicatorRenderer extends JPanel implements ListCellRenderer { - boolean startLoop, midLoop, endLoop; - RowHeaderRenderer(JTable table) + LoopIndicatorRenderer(JTable table) { /*JTableHeader header = table.getTableHeader(); setOpaque(true); @@ -170,8 +128,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable setFont(header.getFont());*/ } - public Component getListCellRendererComponent( JList list, - Object value, int index, boolean isSelected, boolean cellHasFocus) + public Component getListCellRendererComponent(JList list, Object value, int index, boolean isSelected, boolean cellHasFocus) { //setText((value == null) ? "" : value.toString()); //setBorder(new LineBorder(Color.black, 1)); @@ -276,7 +233,9 @@ public class GUISimulatorPathTable extends GUIGroupedTable } } - class RowHeaderListModel extends AbstractListModel + // Model for list representing loop indicator + + class LoopIndicatorListModel extends AbstractListModel { public Object getElementAt(int index) @@ -289,13 +248,15 @@ public class GUISimulatorPathTable extends GUIGroupedTable return ptm.getRowCount(); } - public void updateHeader() + public void updateIndicator() { fireContentsChanged(this, 0, ptm.getRowCount()); } } + // Renderer for cells in path table + class PathChangeCellRenderer extends JPanel { private PathChangeTableRenderer pctr; @@ -381,104 +342,116 @@ public class GUISimulatorPathTable extends GUIGroupedTable public void paintComponent(Graphics g) { super.paintComponent(g); - + + Rectangle rect; + int width, height, x, y; + + // Get graphics context Graphics2D g2 = (Graphics2D)g; - - if (value instanceof String) - { - double width = getStringWidth(stringValue, g2); - double height = g2.getFont().getSize(); - + // Get some info about the string + rect = getStringBounds(stringValue, g2); + width = (int)Math.ceil(rect.getWidth()); + height = (int)Math.ceil(rect.getHeight()); + + // State index + if (value instanceof String) { + // Position (horiz centred, vert centred) + x = (getWidth()/2) - (width/2); + y = (getHeight()/2) + (height/2); + // Write value g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); - g2.setColor(Color.black); - g2.drawString(stringValue, (int)((getWidth()/2 + 0.5)- (width/2)), 12); + g2.drawString(stringValue, x, y); } - else if (value instanceof GUISimulator.VariableValue) - { + // Variable value + else if (value instanceof GUISimulator.VariableValue) { GUISimulator.VariableValue variableValue = (GUISimulator.VariableValue)value; - - double width = getStringWidth(stringValue, g2); - - RoundRectangle2D.Double rec = new RoundRectangle2D.Double((getWidth()/2)-(width/2)-5, 1, width+10, getHeight()-3, 8, 8); - + // Position (horiz centred, vert centred) + x = (getWidth()/2) - (width/2); + y = (getHeight()/2) + (height/2); + // Prepare box/colour + RoundRectangle2D.Double rec = new RoundRectangle2D.Double(x-5, 2, width+10, getHeight()-5, 8, 8); Color color = (variableValue.hasChanged()) ? (Color.black) : (Color.lightGray); - - if (pctr.onlyShowChange()) - { + // "Render changes" view + if (pctr.onlyShowChange()) { + // Vertical line in background g2.setColor(Color.black); g2.drawLine(getWidth()/2, 0, getWidth()/2, getHeight()); - - if (isSelected || variableValue.hasChanged()) - { + // Only display box/value if there was a change + if (isSelected || variableValue.hasChanged()) { g2.setColor(Color.white); g2.fill(rec); - g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON); - g2.setColor(color); g2.draw(rec); - g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); - - g2.drawString(stringValue, (int)((getWidth()/2 + 0.5)- (width/2)), 12); + g2.drawString(stringValue, x, y); } } - else - { + // "Render all values" view + else { + // Just display value g2.setColor(color); g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); - g2.drawString(stringValue, (int)((getWidth()/2 + 0.5)- (width/2)), 12); + g2.drawString(stringValue, x, y); } } - else if (value instanceof GUISimulator.RewardStructureValue) - { + // Reward value + else if (value instanceof GUISimulator.RewardStructureValue) { GUISimulator.RewardStructureValue rewardValue = (GUISimulator.RewardStructureValue)value; - - double width = getStringWidth(stringValue, g2); - - RoundRectangle2D.Double rec = new RoundRectangle2D.Double((getWidth()/2)-(width/2)-5, 1, width+10, getHeight()-3, 8, 8); - - Color color = (rewardValue.hasChanged() || rewardValue.isRewardValueUnknown()) ? (Color.black) : (Color.lightGray); - - if (pctr.onlyShowChange()) - { - g2.setColor(Color.black); - g2.drawLine(getWidth()/2, 0, getWidth()/2, getHeight()); - - if ((isSelected || rewardValue.hasChanged())) - { - g2.setColor(Color.white); - g2.fill(rec); - - g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON); - - g2.setColor(color); - g2.draw(rec); - + // Default case (everything except cumulative for CTMCs) + if (!(ptm.getView().canShowTime() && rewardValue.getRewardStructureColumn().isCumulativeReward())) { + // Position (horiz centred, vert centred) + x = (getWidth()/2) - (width/2); + y = (getHeight()/2) + (height/2); + // Prepare box/colour + RoundRectangle2D.Double rec = new RoundRectangle2D.Double(x-5, 2, width+10, getHeight()-5, 8, 8); + Color color = (rewardValue.hasChanged() || rewardValue.isRewardValueUnknown()) ? (Color.black) : (Color.lightGray); + // "Render changes" view + if (pctr.onlyShowChange()) { + // Vertical line in background + g2.setColor(Color.black); + g2.drawLine(getWidth()/2, 0, getWidth()/2, getHeight()); + // Only display box/value if there was a change + if ((isSelected || rewardValue.hasChanged())) { + g2.setColor(Color.white); + g2.fill(rec); + g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON); + g2.setColor(color); + g2.draw(rec); + g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); + g2.drawString(stringValue, x, y); + } + } + // "Render all values" view + else { + // Just display value + g2.setColor(color); g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); - - g2.drawString(stringValue, (int)((getWidth()/2 + 0.5)- (width/2)), 12); + g2.drawString(stringValue, x, y); } } - else - { - g2.setColor(color); - g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); - g2.drawString(stringValue, (int)((getWidth()/2 + 0.5)- (width/2)), 12); - } + // For cumulative rewards on CTMCs, we left-align (like for display of time) + else { + // Position (left aligned, vert centred) + x = 3; + y = (getHeight()/2) + (height/2); + // Write text + g2.setColor(Color.black); + g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); + g2.drawString(stringValue, x, y); + } } + // Time value else if (value instanceof GUISimulator.TimeValue) { - GUISimulator.TimeValue timeValue = (GUISimulator.TimeValue)value; - - double width = getStringWidth(stringValue, g2); - - Color color = (Color.black); - - g2.setColor(color); + // Position (left aligned, vert centred) + x = 3; + y = (getHeight()/2) + (height/2); + // Write text + g2.setColor(Color.black); g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_OFF); - g2.drawString(stringValue, 3, 12); + g2.drawString(stringValue, x, y); } } } @@ -535,17 +508,30 @@ public class GUISimulatorPathTable extends GUIGroupedTable } } - /** Method which computes width of a string for a given Graphics2D object + /** Method which computes rectangle bounds of a string for a given Graphics2D object */ - public static double getStringWidth(String s, Graphics2D g2) + public static Rectangle getStringBounds(String s, Graphics2D g2) { // catch special cases... // ...TextLayout constructor crashes with null or zero-length string - if (s == null) return 0; - if (s.length() == 0) return 0; + if (s == null) return new Rectangle(0, 0); + if (s.length() == 0) return new Rectangle(0, 0); TextLayout layout = new TextLayout(s, g2.getFont(), g2.getFontRenderContext()); - Rectangle r = layout.getOutline(new AffineTransform()).getBounds(); - return r.getWidth(); + return layout.getOutline(new AffineTransform()).getBounds(); + } + + /** Method which computes width of a string for a given Graphics2D object + */ + public static double getStringWidth(String s, Graphics2D g2) + { + return getStringBounds(s, g2).getWidth(); + } + + /** Method which computes height of a string for a given Graphics2D object + */ + public static double getStringHeight(String s, Graphics2D g2) + { + return getStringBounds(s, g2).getHeight(); } } diff --git a/prism/src/userinterface/simulator/GUISimulatorUpdatesTable.java b/prism/src/userinterface/simulator/GUISimulatorUpdatesTable.java index e95b1f40..6393222c 100644 --- a/prism/src/userinterface/simulator/GUISimulatorUpdatesTable.java +++ b/prism/src/userinterface/simulator/GUISimulatorUpdatesTable.java @@ -3,6 +3,7 @@ // Copyright (c) 2002- // Authors: // * Andrew Hinton (University of Birmingham) +// * Dave Parker (University of Birmingham) // //------------------------------------------------------------------------------ // @@ -54,6 +55,8 @@ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionLis private UpdateHeaderListModel headerModel; private JList header; + private UpdateHeaderRenderer updateHeaderRenderer; + private UpdateTableRenderer updateTableRenderer; private GUISimulator sim; @@ -79,11 +82,13 @@ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionLis rowHeader.setFixedCellHeight(getRowHeight()); //+ getRowMargin()); //getIntercellSpacing().height); - rowHeader.setCellRenderer(new UpdateHeaderRenderer(this)); + updateHeaderRenderer = new UpdateHeaderRenderer(this); + rowHeader.setCellRenderer(updateHeaderRenderer); this.header = rowHeader; - - setDefaultRenderer(Object.class, new UpdateTableRenderer()); + + updateTableRenderer = new UpdateTableRenderer(); + setDefaultRenderer(Object.class, updateTableRenderer); setAutoResizeMode(JTable.AUTO_RESIZE_LAST_COLUMN); @@ -131,6 +136,15 @@ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionLis } + /** Override set font to pass changes onto renderer(s) and set row height */ + public void setFont(Font font) + { + super.setFont(font); + if (updateTableRenderer != null) updateTableRenderer.setFont(font); + setRowHeight(getFontMetrics(font).getHeight() + 4); + if (header != null) header.setFixedCellHeight(getRowHeight()); + } + public void valueChanged(ListSelectionEvent e) { if(headerModel != null) @@ -145,54 +159,58 @@ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionLis class UpdateTableRenderer implements TableCellRenderer { - JTextField renderer; - - - public UpdateTableRenderer() - { - renderer = new JTextField(""); - } - public Component getTableCellRendererComponent(JTable table, Object value, - boolean isSelected, boolean hasFocus, int row, int column) - { - renderer.setText(value.toString()); - - int dist; - - if(sim.getModulesFile().getType() == ModulesFile.STOCHASTIC) - dist = 0; - else dist = utm.getProbabilityDistributionOf(row); - - Color c = DISTRIBUTION_COLOURS[dist%2]; - - - if(isSelected) - { - Color newCol = new Color(c.getRed()-20, c.getGreen()-20, c.getBlue()); - if(utm.oldUpdate) + JTextField renderer; + + public UpdateTableRenderer() { - newCol = new Color(newCol.getRed()-7, newCol.getGreen()-7, newCol.getBlue()-7); - renderer.setBackground(newCol); + renderer = new JTextField(""); } - else + + public Component getTableCellRendererComponent(JTable table, Object value, boolean isSelected, boolean hasFocus, int row, int column) { - renderer.setBackground(newCol); + renderer.setText(value.toString()); + + int dist; + + if(sim.getModulesFile().getType() == ModulesFile.STOCHASTIC) + dist = 0; + else dist = utm.getProbabilityDistributionOf(row); + + Color c = DISTRIBUTION_COLOURS[dist%2]; + + + if(isSelected) + { + Color newCol = new Color(c.getRed()-20, c.getGreen()-20, c.getBlue()); + if(utm.oldUpdate) + { + newCol = new Color(newCol.getRed()-7, newCol.getGreen()-7, newCol.getBlue()-7); + renderer.setBackground(newCol); + } + else + { + renderer.setBackground(newCol); + } + } + else + { + if(utm.oldUpdate) + { + Color newCol = new Color(c.getRed()-7, c.getGreen()-7, c.getBlue()-7); + renderer.setBackground(newCol); + } + else + renderer.setBackground(c); + } + + renderer.setBorder(new EmptyBorder(1, 1, 1, 1)); + return renderer; } - } - else - { - if(utm.oldUpdate) + + public void setFont(Font font) { - Color newCol = new Color(c.getRed()-7, c.getGreen()-7, c.getBlue()-7); - renderer.setBackground(newCol); + renderer.setFont(font); } - else - renderer.setBackground(c); - } - - renderer.setBorder(new EmptyBorder(1, 1, 1, 1)); - return renderer; - } } @@ -222,6 +240,7 @@ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionLis Object value, int index, boolean isSelected, boolean cellHasFocus) { + setBorder(null); selected = getSelectedRow() == index; if(selected) @@ -244,7 +263,7 @@ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionLis public Object getElementAt(int index) { - return ""; + return ""+index; } public int getSize() diff --git a/prism/src/userinterface/util/GUIGroupedTable.java b/prism/src/userinterface/util/GUIGroupedTable.java index 40e490f3..7a89f1b0 100644 --- a/prism/src/userinterface/util/GUIGroupedTable.java +++ b/prism/src/userinterface/util/GUIGroupedTable.java @@ -26,6 +26,8 @@ package userinterface.util; +import java.awt.*; +import java.awt.font.*; import javax.swing.*; import javax.swing.table.*; @@ -123,7 +125,13 @@ public class GUIGroupedTable extends JTable return header; } + + /** Override set font to set row height(s) */ + @Override + public void setFont(Font font) + { + super.setFont(font); + setRowHeight(getFontMetrics(font).getHeight() + 4); + } } - -