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: package de.uka.ilkd.key.gui;
011:
012: import java.awt.BorderLayout;
013: import java.awt.Component;
014: import java.awt.Font;
015: import java.awt.event.*;
016: import java.io.File;
017: import java.util.LinkedList;
018:
019: import javax.swing.*;
020: import javax.swing.tree.DefaultTreeCellRenderer;
021: import javax.swing.tree.TreePath;
022:
023: import de.uka.ilkd.key.gui.configuration.Config;
024: import de.uka.ilkd.key.gui.notification.events.AbandonTaskEvent;
025: import de.uka.ilkd.key.proof.*;
026: import de.uka.ilkd.key.proof.mgt.*;
027: import de.uka.ilkd.key.util.Debug;
028:
029: public class TaskTree extends JPanel {
030:
031: private JTree delegateView;
032:
033: /** the KeYMediator */
034: private KeYMediator mediator;
035:
036: /** listener for mouse events of this gui component */
037: private MouseListener mouseListener = new TaskTreeMouseListener();
038:
039: /** listener to the prof tree events */
040: private ProofTreeListener proofTreeListener = new TaskTreeProofTreeListener();
041:
042: /** the list model to be used */
043: private TaskTreeModel model = new TaskTreeModel();
044:
045: public TaskTree(KeYMediator mediator) {
046: super ();
047: this .mediator = mediator;
048: mediator
049: .addKeYSelectionListener(new TaskTreeSelectionListener());
050: delegateView = new JTree();
051: delegateView.setModel(model);
052: delegateView.setCellRenderer(new TaskTreeIconCellRenderer());
053: delegateView.addMouseListener(mouseListener);
054: this .setLayout(new BorderLayout());
055: this .add(delegateView, BorderLayout.CENTER);
056: delegateView.setShowsRootHandles(false);
057: delegateView.setRootVisible(false);
058: delegateView.putClientProperty("JTree.lineStyle", "Horizontal");
059: }
060:
061: JTree jtree() {
062: return delegateView;
063: }
064:
065: public void addProof(de.uka.ilkd.key.proof.ProofAggregate plist) {
066: TaskTreeNode bp = model.addProof(plist);
067: Proof[] proofs = plist.getProofs();
068: for (int i = 0; i < proofs.length; i++) {
069: proofs[i].addProofTreeListener(proofTreeListener);
070: }
071: delegateView.validate();
072: delegateView.scrollPathToVisible(new TreePath(bp.getPath()));
073: delegateView.setVisible(true);
074: setVisible(true);
075: }
076:
077: public void removeTask(TaskTreeNode tn) {
078:
079: int option = JOptionPane.showConfirmDialog(
080: mediator.mainFrame(), "Are you sure?\n",
081: "Abandon Proof", JOptionPane.YES_NO_OPTION);
082:
083: if (option == JOptionPane.YES_OPTION) {
084: removeTaskWithoutInteraction(tn);
085: }
086: }
087:
088: public void removeTaskWithoutInteraction(TaskTreeNode tn) {
089: model.removeTask(tn);
090: mediator.notify(new AbandonTaskEvent());
091: for (int i = 0; i < tn.allProofs().length; i++) {
092: tn.allProofs()[i]
093: .removeProofTreeListener(proofTreeListener);
094: }
095: //go to some other node, take the last leaf.
096: TreePath path = delegateView.getPathForRow(delegateView
097: .getRowCount() - 1);
098: if (path != null) {
099: TaskTreeNode tn0 = (TaskTreeNode) path
100: .getLastPathComponent();
101: mediator.setProof(tn0.proof());
102: } else {
103: mediator.setProof(null);
104: }
105: }
106:
107: public void updateUI() {
108: super .updateUI();
109: Font myFont = UIManager
110: .getFont(Config.KEY_FONT_PROOF_LIST_VIEW);
111: if (myFont != null) {
112: setFont(myFont);
113: } else {
114: Debug.out(Config.KEY_FONT_PROOF_LIST_VIEW
115: + " not available, use standard font.");
116: }
117: }
118:
119: /** returns the first selected task which is instance of a task tree node
120: */
121: public TaskTreeNode getSelectedTask() {
122: TreePath path = delegateView.getSelectionModel()
123: .getSelectionPath();
124: if (path != null
125: && path.getLastPathComponent() instanceof TaskTreeNode) {
126: return (TaskTreeNode) path.getLastPathComponent();
127: } else {
128: return null;
129: }
130: }
131:
132: /** returns all selected basic tasks */
133: public BasicTask[] getAllSelectedBasicTasks() {
134: LinkedList result = new LinkedList();
135: TreePath[] paths = delegateView.getSelectionModel()
136: .getSelectionPaths();
137: if (paths == null)
138: return new BasicTask[0];
139: for (int i = 0; i < paths.length; i++) {
140: if (paths[i].getLastPathComponent() instanceof BasicTask) {
141: result.add(paths[i].getLastPathComponent());
142: }
143: }
144: return (BasicTask[]) result.toArray(new BasicTask[0]);
145: }
146:
147: /** called when the user has clicked on a problem */
148: private void problemChosen() {
149: TaskTreeNode prob = getSelectedTask();
150: if (prob != null && prob.proof() != null && mediator != null) {
151: mediator.setProof(prob.proof());
152: }
153: }
154:
155: public void removeProof(Proof p) {
156: // %% not implemented
157: }
158:
159: /** inner class implementing the mouse listener that is responsible for
160: * this gui component
161: */
162: class TaskTreeMouseListener extends MouseAdapter {
163:
164: public void mouseClicked(MouseEvent e) {
165: if (e.getClickCount() == 1
166: && e.getModifiers() != (MouseEvent.CTRL_MASK + MouseEvent.BUTTON1_MASK)) {
167: problemChosen();
168: }
169: }
170:
171: public void mousePressed(MouseEvent e) {
172: if (e.isPopupTrigger()) {
173: TreePath selPath = delegateView.getPathForLocation(e
174: .getX(), e.getY());
175: if (selPath != null
176: && selPath.getLastPathComponent() instanceof EnvNode) {
177: JPopupMenu popup = new ProofEnvPopupMenu(
178: ((EnvNode) selPath.getLastPathComponent()));
179: popup.show(e.getComponent(), e.getX(), e.getY());
180: }
181: if (selPath != null
182: && selPath.getLastPathComponent() instanceof BasicTask) {
183: JPopupMenu popup = new BasicTaskPopupMenu(
184: ((BasicTask) selPath.getLastPathComponent()));
185: popup.show(e.getComponent(), e.getX(), e.getY());
186: }
187:
188: }
189: }
190:
191: public void mouseReleased(MouseEvent e) {
192: mousePressed(e);
193: }
194: }
195:
196: /** a prooftree listener, so that it is known when the proof has closed
197: */
198: class TaskTreeProofTreeListener extends ProofTreeAdapter {
199:
200: /** invoked if all goals of the proof are closed
201: */
202: public void proofClosed(ProofTreeEvent e) {
203: delegateView.repaint();
204: }
205:
206: /** invoked if the list of goals changed (goals were added,
207: * removed etc.
208: */
209: public void proofGoalRemoved(ProofTreeEvent e) {
210: }
211:
212: /** invoked if the current goal of the proof changed */
213: public void proofGoalsAdded(ProofTreeEvent e) {
214: }
215:
216: /** invoked if the current goal of the proof changed */
217: public void proofGoalsChanged(ProofTreeEvent e) {
218: }
219: } // end of prooftreelistener
220:
221: static class TaskTreeIconCellRenderer extends
222: DefaultTreeCellRenderer implements java.io.Serializable {
223:
224: static final ImageIcon keyIcon = IconFactory.keyHole(20, 20);
225: static final ImageIcon keyClosedIcon = IconFactory
226: .keyHoleClosed(20, 20);
227: static final ImageIcon keyAlmostClosedIcon = IconFactory
228: .keyHoleAlmostClosed(20, 20);
229:
230: public TaskTreeIconCellRenderer() {
231: setToolTipText("Task");
232: }
233:
234: public Component getTreeCellRendererComponent(JTree list,
235: Object value, boolean selected, boolean expanded,
236: boolean leaf, int row, boolean hasFocus) {
237: Object newValue;
238: if (value instanceof TaskTreeNode) {
239: newValue = ((TaskTreeNode) value).shortDescr();
240: } else {
241: newValue = value;
242: }
243: DefaultTreeCellRenderer sup = (DefaultTreeCellRenderer) super
244: .getTreeCellRendererComponent(list, newValue,
245: selected, expanded, leaf, row, hasFocus);
246: sup.setIcon(null);
247: if (value instanceof TaskTreeNode) {
248: ProofStatus ps = ((TaskTreeNode) value).getStatus();
249: if (ps != null) {
250: if (ps.getProofClosed())
251: sup.setIcon(keyClosedIcon);
252: if (ps.getProofClosedButLemmasLeft())
253: sup.setIcon(keyAlmostClosedIcon);
254: if (ps.getProofOpen())
255: sup.setIcon(keyIcon);
256: }
257:
258: }
259: return sup;
260: }
261: }
262:
263: class ProofEnvPopupMenu extends JPopupMenu implements
264: ActionListener {
265:
266: private JMenuItem diffLast = new JMenuItem("Diff Last Env");
267:
268: private EnvNode invokedNode;
269:
270: public ProofEnvPopupMenu(EnvNode node) {
271: super ("Choose Action");
272: invokedNode = node;
273: create();
274: }
275:
276: private void create() {
277: this .add(diffLast);
278: diffLast.addActionListener(this );
279: }
280:
281: public void actionPerformed(ActionEvent e) {
282: if (e.getSource() == diffLast) {
283: String s = invokedNode.getDiffToLast();
284: JScrollPane scroll = new JScrollPane();
285: JTextArea text = new JTextArea(s, 20, 40);
286: text.setEditable(false);
287: text.setCaretPosition(0);
288: scroll.setViewportView(text);
289: JFrame fr = new JFrame("Diff to Last Proof Environemnt");
290: fr.getContentPane().setLayout(new BorderLayout());
291: fr.getContentPane().add(scroll, BorderLayout.CENTER);
292: JButton ok = new JButton("OK");
293: ok.addActionListener(new ActionListener() {
294: public void actionPerformed(ActionEvent ae) {
295: ((JFrame) ((JButton) ae.getSource())
296: .getTopLevelAncestor()).dispose();
297: }
298: });
299: fr.getContentPane().add(ok, BorderLayout.SOUTH);
300: fr.setSize(600, 900);
301: fr.getContentPane().add(scroll);
302: fr.setVisible(true);
303: }
304: }
305:
306: }
307:
308: class BasicTaskPopupMenu extends JPopupMenu implements
309: ActionListener {
310:
311: private JMenuItem mcList = new JMenuItem(
312: "Show Used Specifications");
313: private JMenuItem loadProof = new JMenuItem(
314: "Load Proof from File");
315: private JMenuItem removeTask = new JMenuItem("Abandon Task");
316:
317: private BasicTask invokedNode;
318:
319: public BasicTaskPopupMenu(BasicTask node) {
320: super ("Choose Action");
321: invokedNode = node;
322: create();
323: }
324:
325: private void create() {
326: this .add(mcList);
327: mcList.addActionListener(this );
328: this .add(loadProof);
329: loadProof.addActionListener(this );
330: this .add(removeTask);
331: removeTask.addActionListener(this );
332: }
333:
334: public void actionPerformed(ActionEvent e) {
335: if (e.getSource() == mcList) {
336: JDialog fr = new UsedMethodContractsList(invokedNode,
337: mediator);
338: fr.setVisible(true);
339: } else if (e.getSource() == removeTask) {
340: removeTask(invokedNode);
341: } else if (e.getSource() == loadProof) {
342: Main mainFrame = Main.getInstance();
343: KeYFileChooser localFileChooser = Main
344: .getFileChooser("Choose file from which to load proof...");
345:
346: boolean loaded = localFileChooser
347: .showOpenDialog(mainFrame);
348: if (loaded) {
349: File file = localFileChooser.getSelectedFile();
350: (new ProblemLoader(file, mainFrame, mediator
351: .getProfile(), true)).run();
352: }
353: }
354: }
355: }
356:
357: class TaskTreeSelectionListener implements KeYSelectionListener {
358: /** focused node has changed */
359: public void selectedNodeChanged(KeYSelectionEvent e) {
360: // empty
361: }
362:
363: /** the selected proof has changed (e.g. a new proof has been
364: * loaded)
365: */
366: public void selectedProofChanged(KeYSelectionEvent e) {
367: if (e.getSource().getSelectedProof() == null) {
368: return;
369: }
370: TaskTreeNode ttn = model.getTaskForProof(e.getSource()
371: .getSelectedProof());
372: jtree().setSelectionPath(new TreePath(ttn.getPath()));
373: validate();
374: }
375:
376: }
377:
378: } // end of TaskTree
|