Added (commented out) experimental code to make graph axes display only odd numbers.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1637 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/userinterface/graph/AxisSettings.java

@@ -907,7 +907,12 @@ public class AxisSettings extends Observable implements SettingOwner
 				if (gridInterval.getDoubleValue() != numAxis.getTickUnit().getSize())
 				{
 					// FIXME: With i.e. interval 0.01 it rounds "0.10" to "0.1"
-					numAxis.setTickUnit(new NumberTickUnit(gridInterval.getDoubleValue()));
+					numAxis.setTickUnit(new NumberTickUnit(gridInterval.getDoubleValue()));
+					// Some experimental code to make axis display only odd numbers:
+					/*if (axisShouldOnlyShowOdd) numAxis.setNumberFormatOverride(new DecimalFormat()
+					{ public StringBuffer format(double number, StringBuffer toAppendTo, FieldPosition pos) {
+							return ((int)number % 2 == 0) ? new StringBuffer("") : super.format(number, toAppendTo, pos);
+					} });*/
 				}
 			}
 		}