Browse Source

Updates to various GUI components for better behaviour under font size changes.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@515 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 19 years ago
parent
commit
c054c3d19f
  1. 8
      prism/src/settings/SettingTable.java
  2. 2
      prism/src/userinterface/GUIConstantsPicker.java
  3. 2
      prism/src/userinterface/GUIPrism.java
  4. 6
      prism/src/userinterface/properties/ConstantHeader.java
  5. 1
      prism/src/userinterface/properties/ConstantLine.java
  6. 7
      prism/src/userinterface/properties/GUIExperimentTable.java
  7. 7
      prism/src/userinterface/properties/GUIPropConstantList.java
  8. 7
      prism/src/userinterface/properties/GUIPropLabelList.java
  9. 9
      prism/src/userinterface/properties/GUIPropertiesList.java
  10. 1
      prism/src/userinterface/properties/GUIResultsTable.java
  11. 6
      prism/src/userinterface/properties/GraphConstantHeader.java
  12. 3
      prism/src/userinterface/simulator/GUIInitialStatePicker.java
  13. 10
      prism/src/userinterface/simulator/GUISimulator.java
  14. 286
      prism/src/userinterface/simulator/GUISimulatorPathTable.java
  15. 111
      prism/src/userinterface/simulator/GUISimulatorUpdatesTable.java
  16. 12
      prism/src/userinterface/util/GUIGroupedTable.java

8
prism/src/settings/SettingTable.java

@ -3,6 +3,7 @@
// Copyright (c) 2002-
// Authors:
// * Andrew Hinton <ug60axh@cs.bham.uc.uk> (University of Birmingham)
// * Dave Parker <dxp@cs.bham.uc.uk> (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");

2
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();

2
prism/src/userinterface/GUIPrism.java

@ -378,6 +378,8 @@ public class GUIPrism extends JFrame
}
}
SwingUtilities.updateComponentTreeUI(this);
SwingUtilities.updateComponentTreeUI(choose);
SwingUtilities.updateComponentTreeUI(options);
repaint();
}

6
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

1
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();

7
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()

7
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();

7
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)

9
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

1
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();

6
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)

3
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

10
prism/src/userinterface/simulator/GUISimulator.java

@ -4,6 +4,7 @@
// Authors:
// * Andrew Hinton <ug60axh@cs.bham.uc.uk> (University of Birmingham)
// * Mark Kattenbelt <mxk@cs.bham.uc.uk> (University of Birmingham)
// * Dave Parker <dxp@cs.bham.uc.uk> (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
}// </editor-fold>//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

286
prism/src/userinterface/simulator/GUISimulatorPathTable.java

@ -4,6 +4,7 @@
// Authors:
// * Andrew Hinton <ug60axh@cs.bham.uc.uk> (University of Birmingham)
// * Mark Kattenbelt <mxk@cs.bham.uc.uk> (University of Birmingham)
// * Dave Parker <dxp@cs.bham.uc.uk> (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();
}
}

111
prism/src/userinterface/simulator/GUISimulatorUpdatesTable.java

@ -3,6 +3,7 @@
// Copyright (c) 2002-
// Authors:
// * Andrew Hinton <ug60axh@cs.bham.uc.uk> (University of Birmingham)
// * Dave Parker <dxp@cs.bham.uc.uk> (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()

12
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);
}
}
Loading…
Cancel
Save