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: import de.uka.ilkd.key.proof.ProofAggregate;
18: import de.uka.ilkd.key.proof.SingleProof;
19:
20: public class ProofAggregateTask extends DefaultMutableTreeNode
21: implements TaskTreeNode {
22:
23: private TaskTreeNode[] proofs;
24: private ProofAggregate proofList;
25: private String descr;
26:
27: public ProofAggregateTask(ProofAggregate ps) {
28: super (ps);
29: proofs = new TaskTreeNode[ps.size()];
30: for (int i = 0; i < ps.size(); i++) {
31: if (ps.getChildren()[i] instanceof SingleProof) {
32: proofs[i] = new BasicTask(ps.getChildren()[i]);
33: } else {
34: proofs[i] = new ProofAggregateTask(ps.getChildren()[i]);
35: }
36: }
37: proofList = ps;
38: descr = ps.description();
39: }
40:
41: public String shortDescr() {
42: return descr;
43: }
44:
45: public String toString() {
46: return shortDescr();
47: }
48:
49: public ProofEnvironment getProofEnv() {
50: return proofs[0].proof().env();
51: }
52:
53: public ProofAggregate getProofList() {
54: return proofList;
55: }
56:
57: public Proof proof() {
58: return proofs[0].proof();
59: }
60:
61: public Proof[] allProofs() {
62: return getProofList().getProofs();
63: }
64:
65: public void insertNode(TaskTreeModel model,
66: MutableTreeNode parentNode) {
67: model.insertNodeInto(this , parentNode, model
68: .getChildCount(parentNode));
69: for (int i = 0; i < proofs.length; i++) {
70: proofs[i].insertNode(model, this );
71: }
72: }
73:
74: public ProofStatus getStatus() {
75: return proofList.getStatus();
76: }
77:
78: public void decoupleFromEnv() {
79: getProofEnv().removeProofList(proofList);
80: }
81: }
|