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.awt.BorderLayout;
014: import java.awt.Component;
015: import java.awt.FlowLayout;
016:
017: import javax.swing.JPanel;
018: import javax.swing.JTextArea;
019: import javax.swing.JTree;
020: import javax.swing.SwingUtilities;
021: import javax.swing.event.TreeSelectionEvent;
022: import javax.swing.event.TreeSelectionListener;
023: import javax.swing.tree.DefaultMutableTreeNode;
024: import javax.swing.tree.DefaultTreeCellRenderer;
025: import javax.swing.tree.TreeCellRenderer;
026:
027: import de.uka.ilkd.key.proof.RuleTreeModel;
028: import de.uka.ilkd.key.proof.mgt.OldOperationContract;
029: import de.uka.ilkd.key.rule.Taclet;
030:
031: public class RuleView extends JPanel implements TreeSelectionListener,
032: java.io.Serializable {
033:
034: protected RuleTreeModel ruleViewModel = null;
035: protected JTree ruleTree;
036:
037: protected KeYMediator mediator = null;
038:
039: /** Listener for proof changes */
040: protected SelectionListener selectionListener = new SelectionListener();
041:
042: public RuleView() {
043: layoutPane();
044: ruleTree.setCellRenderer(new RuleRenderer());
045: ruleTree.addTreeSelectionListener(this );
046: setVisible(true);
047: }
048:
049: public void valueChanged(TreeSelectionEvent e) {
050: if (ruleTree.getLastSelectedPathComponent() != null) {
051: DefaultMutableTreeNode node = (DefaultMutableTreeNode) ruleTree
052: .getLastSelectedPathComponent();
053: if (node.isLeaf()) {
054: TacletView tv = TacletView.getInstance();
055: tv.showTacletView(node);
056: }
057: }
058: }
059:
060: public void setMediator(KeYMediator p_mediator) {
061: if (mediator != null)
062: unregisterAtMediator();
063:
064: mediator = p_mediator;
065: registerAtMediator();
066: if (mediator != null && mediator.getSelectedProof() != null) {
067: setRuleTreeModel(new RuleTreeModel(mediator
068: .getSelectedGoal()));
069: }
070: }
071:
072: protected void setRuleTreeModel(RuleTreeModel model) {
073:
074: ruleViewModel = model;
075:
076: if (ruleViewModel != null) {
077: ruleTree.setModel(ruleViewModel);
078: }
079: }
080:
081: protected void registerAtMediator() {
082: mediator.addKeYSelectionListener(selectionListener);
083: }
084:
085: protected void unregisterAtMediator() {
086: mediator.removeKeYSelectionListener(selectionListener);
087: }
088:
089: protected void layoutPane() {
090: setLayout(new BorderLayout());
091: ruleTree = new JTree(new String[] { "No proof loaded" });
092: add(ruleTree, BorderLayout.CENTER);
093: }
094:
095: /**
096: * Will be called when this dialog will be closed
097: */
098: protected void closeDlg() {
099: // mediator.freeModalAccess(this);
100: }
101:
102: private class SelectionListener implements KeYSelectionListener {
103:
104: /** focused node has changed */
105: public void selectedNodeChanged(KeYSelectionEvent e) {
106: ruleViewModel.setSelectedGoal(e.getSource()
107: .getSelectedGoal());
108: }
109:
110: /** the selected proof has changed (e.g. a new proof has been
111: * loaded) */
112: public void selectedProofChanged(KeYSelectionEvent e) {
113: Runnable action = new Runnable() {
114: public void run() {
115: if (mediator != null
116: && mediator.getSelectedProof() != null)
117: setRuleTreeModel(new RuleTreeModel(mediator
118: .getSelectedGoal()));
119: }
120: };
121:
122: if (SwingUtilities.isEventDispatchThread())
123: action.run();
124: else
125: SwingUtilities.invokeLater(action);
126: }
127:
128: }
129:
130: class RuleRenderer extends DefaultTreeCellRenderer implements
131: TreeCellRenderer, java.io.Serializable {
132:
133: JPanel panel;
134: JPanel statusPanel;
135: JTextArea text;
136:
137: public RuleRenderer() {
138: FlowLayout lay = new FlowLayout();
139: lay.setAlignment(FlowLayout.LEFT);
140: panel = new JPanel(lay);
141: statusPanel = new JPanel(lay);
142: text = new JTextArea();
143: panel.add(statusPanel);
144: panel.add(text);
145: text.setEditable(false);
146: text.setCaretPosition(0);
147: }
148:
149: public Component getTreeCellRendererComponent(JTree tree,
150: Object value, boolean sel, boolean expanded,
151: boolean leaf, int row, boolean hasFocus) {
152: Component comp = super .getTreeCellRendererComponent(tree,
153: value, sel, expanded, leaf, row, hasFocus);
154:
155: DefaultMutableTreeNode node = (DefaultMutableTreeNode) value;
156:
157: if (node.getUserObject() instanceof OldOperationContract) {
158: OldOperationContract mc = (OldOperationContract) node
159: .getUserObject();
160: comp = MethodContractList.makeMethodContractDisplay(mc,
161: panel, text, statusPanel,
162: sel ? super .backgroundSelectionColor
163: : super .backgroundNonSelectionColor);
164: }
165: if (node.getUserObject() instanceof Taclet) {
166:
167: Taclet t = (Taclet) node.getUserObject();
168: String newValue = t.displayName();
169: if (newValue.equals(node.getParent().toString())) {
170: newValue = t.name().toString(); // differentiated name
171: }
172: return super.getTreeCellRendererComponent(tree,
173: newValue, sel, expanded, leaf, row, hasFocus);
174: }
175: return comp;
176:
177: }
178: }
179:
180: }
|