01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.proof.mgt;
12:
13: import javax.swing.tree.DefaultMutableTreeNode;
14: import javax.swing.tree.MutableTreeNode;
15:
16: import de.uka.ilkd.key.proof.Proof;
17:
18: public class EnvNode extends DefaultMutableTreeNode implements
19: TaskTreeNode {
20:
21: private ProofEnvironment env;
22:
23: public EnvNode(ProofEnvironment e) {
24: super (e);
25: env = e;
26: }
27:
28: public String shortDescr() {
29: return env.description();
30: }
31:
32: public String toString() {
33: return shortDescr();
34: }
35:
36: public ProofEnvironment getProofEnv() {
37: return env;
38: }
39:
40: public Proof proof() {
41: return getChildCount() > 0 ? ((TaskTreeNode) getChildAt(0))
42: .proof() : null;
43: }
44:
45: public Proof[] allProofs() {
46: return new Proof[0];
47: }
48:
49: public void insertNode(TaskTreeModel model,
50: MutableTreeNode parentNode) {
51: model.insertNodeInto(this , parentNode, model
52: .getChildCount(parentNode));
53: }
54:
55: public ProofStatus getStatus() {
56: return null;
57: }
58:
59: public String getDiffToLast() {
60: EnvNode lastSibl = (EnvNode) getPreviousSibling();
61: if (lastSibl == null) {
62: return "First proof environment. Nothing to diff.";
63: }
64: return getProofEnv().getDiffUserInfo(lastSibl.getProofEnv());
65: }
66:
67: public void decoupleFromEnv() {
68: // do nothing
69: }
70:
71: }
|