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 java.util.HashMap;
14: import java.util.Map;
15:
16: import javax.swing.tree.DefaultMutableTreeNode;
17: import javax.swing.tree.DefaultTreeModel;
18: import javax.swing.tree.MutableTreeNode;
19:
20: import de.uka.ilkd.key.proof.Node;
21: import de.uka.ilkd.key.proof.Proof;
22: import de.uka.ilkd.key.proof.ProofAggregate;
23:
24: public class TaskTreeModel extends DefaultTreeModel {
25:
26: private Map proofToTask = new HashMap();
27:
28: public TaskTreeModel() {
29: super (new DefaultMutableTreeNode("Tasks"));
30: }
31:
32: public void addTask(TaskTreeNode p) {
33: ProofEnvironment env = p.getProofEnv();
34: int size = getChildCount(getRoot());
35: for (int i = 0; i < size; i++) {
36: MutableTreeNode envNode = (MutableTreeNode) getChild(
37: getRoot(), i);
38: if (env == ((EnvNode) envNode).getProofEnv()) {
39: p.insertNode(this , envNode);
40: updateProofToTask(p);
41: return;
42: }
43: } //env not present yet
44: EnvNode envNode = new EnvNode(env);
45: insertNodeInto(envNode, (MutableTreeNode) getRoot(), size);
46: updateProofToTask(p);
47: p.insertNode(this , envNode);
48: }
49:
50: public void removeTask(TaskTreeNode p) {
51: Proof[] allProofs = p.allProofs();
52: for (int i = 0; i < allProofs.length; i++) {
53: proofToTask.remove(allProofs[i]);
54: Node.clearReuseCandidates(allProofs[i]); // yes, listeners...
55: p.decoupleFromEnv();
56: }
57: if (p.getParent().getChildCount() == 1) { // remove env if p is single
58: GlobalProofMgt.getInstance().removeEnv(p.getProofEnv());
59: p = (TaskTreeNode) p.getParent();
60: }
61: removeNodeFromParent(p);
62: p.getProofEnv().updateProofStatus(); // this should be done by listeners
63: }
64:
65: private void updateProofToTask(TaskTreeNode p) {
66: Proof[] proofs = p.allProofs();
67: for (int i = 0; i < proofs.length; i++) {
68: proofToTask.put(proofs[i], p);
69: }
70: }
71:
72: public TaskTreeNode getTaskForProof(Proof p) {
73: if (p == null)
74: return null;
75: return p.getBasicTask();
76: }
77:
78: public TaskTreeNode addProof(ProofAggregate plist) {
79: TaskTreeNode bp;
80: if (plist.size() == 1) {
81: bp = new BasicTask(plist);
82: } else {
83: bp = new ProofAggregateTask(plist);
84: }
85: addTask(bp);
86: return bp;
87: }
88:
89: }
|