Browse Source

Fix GUI so that displayed property results (in results dialog, tooltips) respect new lines (e.g. for Pareto properties).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6227 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 13 years ago
parent
commit
3dfc147fc7
  1. 2
      prism/src/userinterface/properties/GUIProperty.java
  2. 2
      prism/src/userinterface/properties/GUIPropertyResultDialog.java

2
prism/src/userinterface/properties/GUIProperty.java

@ -256,7 +256,7 @@ public class GUIProperty
case STATUS_RESULT_ERROR:
return getResultString();
default:
return "Result: " + getResultString();
return "<html>Result: " + getResultString().replaceAll("\n", "<br/>") + "</html>";
}
}

2
prism/src/userinterface/properties/GUIPropertyResultDialog.java

@ -51,7 +51,7 @@ public class GUIPropertyResultDialog extends javax.swing.JDialog
propertyLabel.setText(gp.getPropString());
constantsLabel.setText(gp.getConstantsString());
methodLabel.setText(gp.getMethodString());
resultLabel.setText(gp.getResultString());
resultLabel.setText("<html>" + gp.getResultString().replaceAll("\n", "<br/>") + "</html>");
if (gp.getNumberOfWarnings() == 0) {
warningLabel.setText("");
} else if (gp.getNumberOfWarnings() == 1) {

Loading…
Cancel
Save