001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.gui;
012:
013: import java.util.Hashtable;
014: import java.util.LinkedList;
015: import java.util.Iterator;
016:
017: import javax.swing.BorderFactory;
018: import javax.swing.JLabel;
019: import javax.swing.JSlider;
020: import javax.swing.event.ChangeEvent;
021: import javax.swing.event.ChangeListener;
022:
023: public class MaxRuleAppSlider extends JSlider {
024: private static final int MAX_RULE_APPS_LOG10 = 5;
025: private final static String TEXT = "Max. Rule Applications: ";
026: private KeYMediator mediator;
027: private static LinkedList allInstances = new LinkedList();
028:
029: public MaxRuleAppSlider(KeYMediator mediator) {
030: super (JSlider.HORIZONTAL, 0, MAX_RULE_APPS_LOG10 * 9, 0);
031:
032: this .mediator = mediator;
033:
034: // set up slider labels
035: Hashtable labelTable = new Hashtable();
036:
037: for (int n = 0; n <= MAX_RULE_APPS_LOG10; n++) {
038: int val = (int) Math.pow(10, n);
039: JLabel l = new JLabel("" + val);
040: l.setFont(l.getFont().deriveFont(9F));
041: labelTable.put(new Integer(n * 9), l);
042: }
043:
044: setLabelTable(labelTable);
045: setPaintLabels(true);
046:
047: // show ticks
048: setMajorTickSpacing(9);
049: setMinorTickSpacing(1);
050: setPaintTicks(true);
051:
052: // add change listener
053: addChangeListener(new ChangeListener() {
054: public void stateChanged(ChangeEvent e) {
055: int n = getValue();
056: int major = n / 9;
057: int minor = n % 9;
058: int val = (minor + 1) * (int) Math.pow(10, major);
059: MaxRuleAppSlider.this .mediator
060: .setMaxAutomaticSteps(val);
061: setTitle(val);
062: updateAllSliders();
063: }
064: });
065:
066: setTitle(0);
067:
068: allInstances.add(this );
069: }
070:
071: public void setPos(int maxRuleApps) {
072: if (maxRuleApps > 0) {
073: int major = (int) (Math.log(maxRuleApps) / Math.log(10));
074: int minor = maxRuleApps / (int) Math.pow(10, major) - 1;
075: int initPos = Math.max(0, Math.min(MAX_RULE_APPS_LOG10 * 9,
076: major * 9 + minor));
077: setValue(initPos);
078: }
079: }
080:
081: private void setTitle(int maxRuleApps) {
082: setBorder(BorderFactory.createTitledBorder(TEXT + maxRuleApps));
083: }
084:
085: public void refresh() {
086: final int steps = mediator.getMaxAutomaticSteps();
087: setPos(steps);
088: setTitle(steps);
089: }
090:
091: private void updateAllSliders() {
092: Iterator it = allInstances.iterator();
093: while (it.hasNext()) {
094: ((MaxRuleAppSlider) it.next()).refresh();
095: }
096: }
097:
098: public void setMediator(KeYMediator mediator) {
099: this.mediator = mediator;
100: }
101: }
|