0001: // This file is part of KeY - Integrated Deductive Software Design
0002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
0003: // Universitaet Koblenz-Landau, Germany
0004: // Chalmers University of Technology, Sweden
0005: //
0006: // The KeY system is protected by the GNU General Public License.
0007: // See LICENSE.TXT for details.
0008: //
0009: //
0010:
0011: package de.uka.ilkd.key.gui.prooftree;
0012:
0013: import java.awt.BorderLayout;
0014: import java.awt.Color;
0015: import java.awt.Component;
0016: import java.awt.Font;
0017: import java.awt.event.*;
0018: import java.util.HashSet;
0019: import java.util.Hashtable;
0020: import java.util.Vector;
0021:
0022: import javax.swing.*;
0023: import javax.swing.event.DocumentEvent;
0024: import javax.swing.event.DocumentListener;
0025: import javax.swing.event.TreeModelEvent;
0026: import javax.swing.event.TreeModelListener;
0027: import javax.swing.event.TreeSelectionEvent;
0028: import javax.swing.event.TreeSelectionListener;
0029: import javax.swing.plaf.TreeUI;
0030: import javax.swing.plaf.basic.BasicTreeUI;
0031: import javax.swing.text.Position;
0032: import javax.swing.tree.*;
0033:
0034: import de.uka.ilkd.key.gui.*;
0035: import de.uka.ilkd.key.gui.configuration.Config;
0036: import de.uka.ilkd.key.gui.configuration.ConfigChangeEvent;
0037: import de.uka.ilkd.key.gui.configuration.ConfigChangeListener;
0038: import de.uka.ilkd.key.proof.*;
0039: import de.uka.ilkd.key.util.Debug;
0040:
0041: public class ProofTreeView extends JPanel {
0042:
0043: private static final Color PASTEL_COLOR = new Color(255, 255, 204);
0044: private static final Color BISQUE_COLOR = new Color(240, 228, 196);
0045: private static final Color PALE_RED_COLOR = new Color(255, 153, 153);
0046: private static final Color LIGHT_BLUE_COLOR = new Color(230, 230,
0047: 255);
0048:
0049: /** the mediator is stored here */
0050: private KeYMediator mediator;
0051:
0052: /** The JTree that is used for actual display and interaction */
0053: private final JTree delegateView;
0054:
0055: /** the model that is displayed by the delegateView */
0056: private GUIProofTreeModel delegateModel;
0057:
0058: private Hashtable models = new Hashtable(20);
0059:
0060: /** the proof this view shows */
0061: private Proof proof;
0062:
0063: /** the expansion state of the proof tree */
0064: private ExpansionState expansionState;
0065:
0066: /** listener */
0067: private GUIProofTreeProofListener proofListener;
0068: private GUITreeSelectionListener treeSelectionListener;
0069: private GUIProofTreeGUIListener guiListener;
0070:
0071: /** KeYStroke for the serach panel */
0072: private final static KeyStroke searchKeyStroke = KeyStroke
0073: .getKeyStroke(KeyEvent.VK_F3, 0);
0074:
0075: /**
0076: * Roots of subtrees containing all nodes to which rules have been
0077: * applied; this is used when auto mode is active
0078: */
0079: private ListOfNode modifiedSubtrees = null;
0080: private HashSet modifiedSubtreesCache = null;
0081:
0082: /** the search dialog */
0083: private ProofTreeSearchPanel proofTreeSearchPanel;
0084:
0085: /** creates a new proof tree */
0086: public ProofTreeView(KeYMediator mediator) {
0087:
0088: proofListener = new GUIProofTreeProofListener();
0089: guiListener = new GUIProofTreeGUIListener();
0090: delegateView = new JTree(new DefaultMutableTreeNode(
0091: "No proof loaded")) {
0092: public void updateUI() {
0093: super .updateUI();
0094: /* we want plus/minus signs to expand/collapse tree nodes */
0095: final TreeUI ui = getUI();
0096: if (ui instanceof BasicTreeUI) {
0097: final BasicTreeUI treeUI = (BasicTreeUI) ui;
0098: treeUI.setExpandedIcon(IconFactory.expandedIcon());
0099: treeUI
0100: .setCollapsedIcon(IconFactory
0101: .collapsedIcon());
0102: }
0103: }
0104: };
0105:
0106: delegateView.getInputMap(JComponent.WHEN_FOCUSED).getParent()
0107: .remove(
0108: KeyStroke.getKeyStroke(KeyEvent.VK_UP,
0109: ActionEvent.CTRL_MASK));
0110: delegateView.getInputMap(JComponent.WHEN_FOCUSED).getParent()
0111: .remove(
0112: KeyStroke.getKeyStroke(KeyEvent.VK_DOWN,
0113: ActionEvent.CTRL_MASK));
0114:
0115: delegateView.setInvokesStopCellEditing(true);
0116: delegateView.getSelectionModel().setSelectionMode(
0117: TreeSelectionModel.SINGLE_TREE_SELECTION);
0118: treeSelectionListener = new GUITreeSelectionListener();
0119: delegateView.addTreeSelectionListener(treeSelectionListener);
0120: delegateView.setScrollsOnExpand(true);
0121: ToolTipManager.sharedInstance().registerComponent(delegateView);
0122:
0123: MouseListener ml = new MouseAdapter() {
0124: public void mousePressed(MouseEvent e) {
0125: if (e.isPopupTrigger()) {
0126: TreePath selPath = delegateView.getPathForLocation(
0127: e.getX(), e.getY());
0128: if (selPath != null
0129: && (selPath.getLastPathComponent() instanceof GUIProofTreeNode || selPath
0130: .getLastPathComponent() instanceof GUIBranchNode)) {
0131: JPopupMenu popup = new ProofTreePopupMenu(
0132: selPath);
0133: popup
0134: .show(e.getComponent(), e.getX(), e
0135: .getY());
0136: }
0137: }
0138: }
0139:
0140: public void mouseReleased(MouseEvent e) {
0141: mousePressed(e);
0142: }
0143: };
0144:
0145: delegateView.addMouseListener(ml);
0146:
0147: setMediator(mediator);
0148:
0149: // UIManager.addPropertyChangeListener(
0150: // new PropertyChangeListener() {
0151: // public void propertyChange(PropertyChangeEvent e) {
0152: // if (Config.KEY_FONT_PROOF_TREE.
0153: // equals(e.getPropertyName())) {
0154: // setProofTreeFont();
0155: // }
0156: // }
0157: // });
0158:
0159: Config.DEFAULT
0160: .addConfigChangeListener(new ConfigChangeListener() {
0161: public void configChanged(ConfigChangeEvent e) {
0162: setProofTreeFont();
0163: }
0164: });
0165:
0166: setProofTreeFont();
0167: delegateView.setLargeModel(true);
0168:
0169: updateUI();
0170:
0171: this .setLayout(new BorderLayout());
0172: this .add(new JScrollPane(delegateView), BorderLayout.CENTER);
0173: this .proofTreeSearchPanel = new ProofTreeSearchPanel();
0174: this .add(proofTreeSearchPanel, BorderLayout.SOUTH);
0175:
0176: layoutKeYComponent();
0177:
0178: Proof selProof = mediator.getSelectedProof();
0179: if (selProof != null) {
0180: setProof(selProof);
0181: }
0182:
0183: final ActionListener keyboardAction = new ActionListener() {
0184: public void actionPerformed(ActionEvent e) {
0185: proofTreeSearchPanel.setVisible(true);
0186: }
0187: };
0188:
0189: registerKeyboardAction(keyboardAction, searchKeyStroke,
0190: JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT);
0191: }
0192:
0193: private void setProofTreeFont() {
0194: Font myFont = UIManager.getFont(Config.KEY_FONT_PROOF_TREE);
0195: if (myFont != null) {
0196: delegateView.setFont(myFont);
0197: } else {
0198: Debug.out("KEY-PROOF_TREE_FONT not available, "
0199: + "use standard font.");
0200: }
0201: }
0202:
0203: /** layout the component */
0204: protected void layoutKeYComponent() {
0205: delegateView.setBackground(Color.white);
0206: ProofRenderer renderer = new ProofRenderer();
0207: delegateView.setCellRenderer(renderer);
0208: delegateView.putClientProperty("JTree.lineStyle", "Angled");
0209:
0210: delegateView.setVisible(true);
0211: }
0212:
0213: /** returns the mediator to communicate with the model
0214: * @return the mediator to communicate with the model
0215: */
0216: public KeYMediator mediator() {
0217: return mediator;
0218: }
0219:
0220: /** sets the mediator to communicate with the model */
0221: private void setMediator(KeYMediator m) {
0222: if (mediator != null)
0223: unregister();
0224: mediator = m;
0225: register();
0226: }
0227:
0228: private void register() {
0229: mediator.addKeYSelectionListener(proofListener);
0230: mediator.addAutoModeListener(proofListener);
0231: mediator.addRuleAppListener(proofListener);
0232: mediator.addGUIListener(guiListener);
0233: }
0234:
0235: private void unregister() {
0236: mediator.removeKeYSelectionListener(proofListener);
0237: mediator.removeAutoModeListener(proofListener);
0238: mediator.removeRuleAppListener(proofListener);
0239: mediator.removeGUIListener(guiListener);
0240: }
0241:
0242: public void removeNotify() {
0243: unregister();
0244: try {
0245: delegateModel.unregister();
0246: } catch (NullPointerException e) {
0247: Debug
0248: .out("Exception thrown by class ProofTreeView at unregister()");
0249: }
0250: super .removeNotify();
0251: }
0252:
0253: /**
0254: * sets up the proof tree view if a proof has been loaded
0255: * @param p the Proof that has been loaded
0256: */
0257: private void setProof(Proof p) {
0258: if (delegateModel != null) {
0259: expansionState.disconnect(delegateView);
0260: delegateModel.storeExpansionState(expansionState
0261: .state(new HashSet()));
0262: delegateModel.storeSelection(delegateView
0263: .getSelectionPath());
0264: delegateModel.unregister();
0265: delegateModel.removeTreeModelListener(proofTreeSearchPanel);
0266: }
0267:
0268: proof = p;
0269:
0270: if (proof != null) {
0271: delegateModel = (GUIProofTreeModel) models.get(p);
0272: if (delegateModel == null) {
0273: delegateModel = new GUIProofTreeModel(p);
0274: models.put(p, delegateModel);
0275: }
0276: delegateModel.addTreeModelListener(proofTreeSearchPanel);
0277: delegateModel.register();
0278: delegateView.setModel(delegateModel);
0279: expansionState = new ExpansionState(delegateView,
0280: delegateModel.getExpansionState());
0281: delegateView.expandRow(0);
0282: delegateView.setSelectionPath(delegateModel.getSelection());
0283: delegateView.scrollPathToVisible(delegateModel
0284: .getSelection());
0285: } else {
0286: delegateModel = null;
0287: delegateView.setModel(new DefaultTreeModel(
0288: new DefaultMutableTreeNode("No proof loaded.")));
0289: expansionState = null;
0290: }
0291: proofTreeSearchPanel.reset();
0292: }
0293:
0294: public void removeProof(Proof p) {
0295: models.remove(p);
0296: }
0297:
0298: public void removeProofs(Proof[] p) {
0299: for (int i = 0; i < p.length; i++) {
0300: models.remove(p[i]);
0301: }
0302: }
0303:
0304: /** moves the scope of the tree view to the given node so that it
0305: * is visible
0306: */
0307: public void makeNodeVisible(Node n) {
0308: if (n == null)
0309: return;
0310:
0311: final GUIProofTreeNode node = delegateModel.getProofTreeNode(n);
0312: if (node == null)
0313: return;
0314:
0315: Object[] obs = node.getPath();
0316: TreePath tp = new TreePath(obs);
0317: treeSelectionListener.ignoreChange = true;
0318: delegateView.getSelectionModel().setSelectionPath(tp);
0319: delegateView.scrollPathToVisible(tp);
0320: delegateView.validate();
0321: treeSelectionListener.ignoreChange = false;
0322: }
0323:
0324: protected void makeNodeExpanded(Node n) {
0325: GUIProofTreeNode node = delegateModel.getProofTreeNode(n);
0326: if (node == null)
0327: return;
0328: Object[] obs = node.getPath();
0329: TreePath tp = new TreePath(obs);
0330: delegateView.makeVisible(tp);
0331: }
0332:
0333: /**
0334: * Collapse all subtrees that are closed
0335: */
0336: protected void collapseClosedNodes() {
0337: collapseClosedNodesHelp(new TreePath(delegateModel.getRoot()));
0338: }
0339:
0340: private void collapseClosedNodesHelp(TreePath path) {
0341: if (!delegateView.isExpanded(path))
0342: return;
0343:
0344: Object node = path.getLastPathComponent();
0345:
0346: if (node instanceof GUIBranchNode
0347: && mediator().getUserConstraint().displayClosed(
0348: ((GUIBranchNode) node).getNode())) {
0349: delegateView.collapsePath(path);
0350: return;
0351: }
0352:
0353: for (int count = delegateModel.getChildCount(node), i = 0; i < count; i++) {
0354: Object child = delegateModel.getChild(node, i);
0355: if (!delegateModel.isLeaf(child))
0356: collapseClosedNodesHelp(path.pathByAddingChild(child));
0357: }
0358: }
0359:
0360: /**
0361: * Collapse all branches which are not below <tt>path</tt>
0362: */
0363: protected void collapseOthers(TreePath path) {
0364: collapseOthersHelp(new TreePath(delegateModel.getRoot()), path);
0365: }
0366:
0367: private void collapseOthersHelp(TreePath start, TreePath stop) {
0368: if (!delegateView.isExpanded(start) || start.equals(stop))
0369: return;
0370:
0371: Object node = start.getLastPathComponent();
0372:
0373: if (node instanceof GUIBranchNode && !start.isDescendant(stop)) {
0374: delegateView.collapsePath(start);
0375: return;
0376: }
0377:
0378: for (int count = delegateModel.getChildCount(node), i = 0; i < count; i++) {
0379: Object child = delegateModel.getChild(node, i);
0380: if (!delegateModel.isLeaf(child))
0381: collapseOthersHelp(start.pathByAddingChild(child), stop);
0382: }
0383: }
0384:
0385: /**
0386: * Selects the given Branchnode in the ProofTreeView and displays the
0387: * first child in the main view.
0388: */
0389: private void selectBranchNode(GUIBranchNode node) {
0390: if (node == null) {
0391: return;
0392: }
0393: proofListener.ignoreNodeSelectionChange = true;
0394: mediator.getSelectionModel().setSelectedNode(node.getNode());
0395: proofListener.ignoreNodeSelectionChange = false;
0396: TreePath tp = new TreePath(node.getPath());
0397: treeSelectionListener.ignoreChange = true;
0398: delegateView.getSelectionModel().setSelectionPath(tp);
0399: delegateView.scrollPathToVisible(tp);
0400: delegateView.validate();
0401: treeSelectionListener.ignoreChange = false;
0402: }
0403:
0404: /**
0405: * In auto mode, add a node which has been modified in a way
0406: * leading to structural changes of the proof tree
0407: */
0408: private void addModifiedNode(Node p_node) {
0409: if (modifiedSubtrees == null)
0410: return;
0411:
0412: try {
0413: if (!modifiedSubtrees.isEmpty()) {
0414: Node n = p_node;
0415: while (true) {
0416: if (modifiedSubtreesCache.contains(n))
0417: return;
0418: if (n.root())
0419: break;
0420: n = n.parent();
0421: }
0422: }
0423:
0424: modifiedSubtrees = modifiedSubtrees.prepend(p_node);
0425: } finally {
0426: modifiedSubtreesCache.add(p_node);
0427: }
0428: }
0429:
0430: // INNER CLASSES
0431:
0432: // listens to gui events
0433: class GUIProofTreeGUIListener implements GUIListener,
0434: java.io.Serializable {
0435: /** invoked if a frame that wants modal access is opened */
0436: public void modalDialogOpened(GUIEvent e) {
0437: delegateView.setEnabled(false);
0438: }
0439:
0440: /** invoked if a frame that wants modal access is closed */
0441: public void modalDialogClosed(GUIEvent e) {
0442: delegateView.setEnabled(true);
0443: }
0444:
0445: public void shutDown(GUIEvent e) {
0446:
0447: }
0448: }
0449:
0450: class GUIProofTreeProofListener implements AutoModeListener,
0451: RuleAppListener, KeYSelectionListener {
0452:
0453: /** node of the last known current goal */
0454: private Node lastGoalNode;
0455:
0456: // hack to select Nodes without changing the selection of delegateView
0457: public boolean ignoreNodeSelectionChange = false;
0458:
0459: /** makes selected node visible of lastGoalNode */
0460: public void makeSelectedNodeVisible(Node selectedNode) {
0461:
0462: if (selectedNode != null) {
0463: if (proof != selectedNode.proof()) {
0464: return;
0465: }
0466: lastGoalNode = selectedNode;
0467: }
0468:
0469: makeNodeVisible(lastGoalNode);
0470: delegateView.validate();
0471: }
0472:
0473: /** focused node has changed */
0474: public void selectedNodeChanged(KeYSelectionEvent e) {
0475: if (!ignoreNodeSelectionChange)
0476: makeSelectedNodeVisible(mediator.getSelectedNode());
0477: }
0478:
0479: /** the selected proof has changed (e.g. a new proof has been
0480: * loaded) */
0481: public void selectedProofChanged(KeYSelectionEvent e) {
0482: Debug.out("ProofTreeView: initialize with new proof");
0483: lastGoalNode = null;
0484: setProof(e.getSource().getSelectedProof());
0485: delegateView.validate();
0486: }
0487:
0488: /** invoked if automatic application of rules has started
0489: */
0490: public void autoModeStarted(ProofEvent e) {
0491: modifiedSubtrees = SLListOfNode.EMPTY_LIST;
0492: modifiedSubtreesCache = new HashSet();
0493: if (delegateModel == null) {
0494: Debug.out("delegateModel is null");
0495: return;
0496: }
0497: if (delegateModel.isAttentive()) {
0498: mediator.removeKeYSelectionListener(proofListener);
0499: }
0500: delegateModel.setAttentive(false);
0501: }
0502:
0503: /** invoked if automatic application of rules has stopped
0504: */
0505: public void autoModeStopped(ProofEvent e) {
0506: if (mediator.getSelectedProof() == null)
0507: return; // no proof (yet)
0508: delegateView
0509: .removeTreeSelectionListener(treeSelectionListener);
0510: if (delegateModel == null) {
0511: setProof(mediator.getSelectedProof());
0512: } else if (modifiedSubtrees != null) {
0513: IteratorOfNode it = modifiedSubtrees.iterator();
0514: while (it.hasNext())
0515: delegateModel.updateTree(it.next());
0516: }
0517: if (!delegateModel.isAttentive()) {
0518: delegateModel.setAttentive(true);
0519: mediator.addKeYSelectionListener(proofListener);
0520: }
0521: makeSelectedNodeVisible(mediator.getSelectedNode());
0522: delegateView
0523: .addTreeSelectionListener(treeSelectionListener);
0524: delegateView.validate();
0525: modifiedSubtrees = null;
0526: modifiedSubtreesCache = null;
0527: }
0528:
0529: /** invoked when a rule has been applied */
0530: public void ruleApplied(ProofEvent e) {
0531: addModifiedNode(e.getRuleAppInfo().getOriginalNode());
0532: }
0533:
0534: }
0535:
0536: class GUITreeSelectionListener implements TreeSelectionListener,
0537: java.io.Serializable {
0538: // hack to reduce duplicated repaints
0539: public boolean ignoreChange = false;
0540:
0541: public void valueChanged(TreeSelectionEvent e) {
0542: if (ignoreChange)
0543: return;
0544: if (e.getNewLeadSelectionPath() == null) {
0545: return;
0546: }
0547: // catching ClassCastException occurring when clicking on
0548: // "No proof loaded"
0549: if (!(e.getNewLeadSelectionPath().getLastPathComponent() instanceof GUIAbstractTreeNode)) {
0550: return;
0551: }
0552: GUIAbstractTreeNode treeNode = ((GUIAbstractTreeNode) e
0553: .getNewLeadSelectionPath().getLastPathComponent());
0554: if (treeNode instanceof GUIProofTreeNode) {
0555: Node node = ((GUIProofTreeNode) treeNode).getNode();
0556: Goal selected = proof.getGoal(node);
0557: if (selected != null) {
0558: mediator.goalChosen(selected);
0559: } else {
0560: mediator.nonGoalNodeChosen(node);
0561: }
0562: } else if (treeNode instanceof GUIBranchNode) {
0563: selectBranchNode((GUIBranchNode) treeNode);
0564: }
0565: // catching NullPointerException occurring when renaming root node
0566: if (treeNode instanceof GUIBranchNode
0567: && ((GUIBranchNode) treeNode).getNode().parent() != null) {
0568: delegateView.setEditable(true);
0569: } else {
0570: delegateView.setEditable(false);
0571: }
0572: }
0573: }
0574:
0575: class ProofRenderer extends DefaultTreeCellRenderer implements
0576: TreeCellRenderer, java.io.Serializable {
0577:
0578: public Component getTreeCellRendererComponent(JTree tree,
0579: Object value, boolean sel, boolean expanded,
0580: boolean leaf, int row, boolean hasFocus) {
0581: if (proof == null) {
0582: // print dummy tree;
0583: return super .getTreeCellRendererComponent(tree, value,
0584: sel, expanded, leaf, row, hasFocus);
0585: }
0586:
0587: if (!(value instanceof GUIProofTreeNode)) {
0588: super .getTreeCellRendererComponent(tree, value, sel,
0589: expanded, leaf, row, hasFocus);
0590: setBackgroundNonSelectionColor(BISQUE_COLOR);
0591: if (value instanceof GUIBranchNode) {
0592: if (mediator().getUserConstraint().displayClosed(
0593: ((GUIBranchNode) value).getNode())) {
0594: // all goals below this node are closed
0595: this .setIcon(IconFactory.provedFolderIcon());
0596: } else if (((GUIBranchNode) value).getNode()
0597: .getBranchSink().getResetConstraint()
0598: .isSatisfiable()) {
0599: // a instantiation of the metavariables does
0600: // exist that makes the remaining goals of
0601: // this subtree closed
0602: this .setIcon(IconFactory.closableFolderIcon());
0603: }
0604: }
0605: return this ;
0606: }
0607: Node node = ((GUIProofTreeNode) value).getNode();
0608: String nodeText = node.serialNr() + ":" + node.name();
0609: boolean isBranch = false;
0610:
0611: {
0612: final Node child = ((GUIProofTreeNode) value)
0613: .findChild(node);
0614: if (child != null
0615: && child.getNodeInfo().getBranchLabel() != null) {
0616: nodeText += ": "
0617: + child.getNodeInfo().getBranchLabel();
0618: isBranch = true;
0619: }
0620: }
0621:
0622: DefaultTreeCellRenderer tree_cell = (DefaultTreeCellRenderer) super
0623: .getTreeCellRendererComponent(tree, nodeText, sel,
0624: expanded, leaf, row, hasFocus);
0625:
0626: tree_cell.setFont(tree.getFont());
0627: tree_cell.setText(nodeText);
0628:
0629: if (node.leaf()) {
0630: Goal goal = proof.getGoal(node);
0631: if (goal == null
0632: || mediator().getUserConstraint()
0633: .displayClosed(node)) {
0634: tree_cell.setForeground(Color.green);
0635: tree_cell
0636: .setIcon(IconFactory.keyHoleClosed(20, 20));
0637: ProofTreeView.this .setToolTipText("Closed Goal");
0638: tree_cell.setToolTipText("A closed goal");
0639: } else {
0640: if (goal.getClosureConstraint().isSatisfiable()) {
0641: tree_cell.setForeground(Color.blue);
0642: tree_cell.setIcon(IconFactory.keyHole(20, 20));
0643: ProofTreeView.this
0644: .setToolTipText("Closable Goal");
0645: tree_cell
0646: .setToolTipText("A goal that can be closed");
0647: } else {
0648: tree_cell.setForeground(Color.red);
0649: ProofTreeView.this .setToolTipText("Open Goal");
0650: tree_cell.setToolTipText("An open goal");
0651: }
0652: tree_cell.setIcon(IconFactory.keyHole(20, 20));
0653: }
0654: } else {
0655: /*
0656: if ( node.getBranchSink ().getResetConstraint ().isSatisfiable () )
0657: tree_cell.setForeground(Color.blue);
0658: else
0659: */
0660: tree_cell.setForeground(Color.black);
0661: String tooltipText = "An inner node of the proof";
0662: if (node.isReuseCandidate()) {
0663: tree_cell.setIcon(IconFactory.reuseLogo());
0664: } else {
0665: Icon defaultIcon;
0666: if (node.getNodeInfo()
0667: .getInteractiveRuleApplication()) {
0668: defaultIcon = IconFactory
0669: .interactiveAppLogo(16);
0670: tooltipText = "An inner node (rule applied by user)";
0671: } else {
0672: defaultIcon = null;
0673: }
0674: if (isBranch) {
0675: defaultIcon = getOpenIcon();
0676: tooltipText = "A branch node with all siblings hidden";
0677: }
0678: tree_cell.setIcon(defaultIcon);
0679: }
0680: tree_cell.setToolTipText(tooltipText);
0681: }
0682:
0683: if (node.getReuseSource() != null) {
0684: tree_cell.setBackgroundNonSelectionColor(PASTEL_COLOR);
0685: if (!node.getReuseSource().isConnect()) {
0686: tree_cell
0687: .setBackgroundNonSelectionColor(PALE_RED_COLOR);
0688: }
0689: } else if (node.getNodeInfo().getActiveStatement() != null) {
0690: tree_cell
0691: .setBackgroundNonSelectionColor(LIGHT_BLUE_COLOR);
0692:
0693: } else {
0694: tree_cell.setBackgroundNonSelectionColor(Color.white);
0695: }
0696: if (sel)
0697: tree_cell.setBackground(Color.blue);
0698:
0699: return tree_cell;
0700: }
0701: }
0702:
0703: class ProofTreePopupMenu extends JPopupMenu implements
0704: ActionListener, ItemListener {
0705:
0706: private JMenuItem expandAll = new JMenuItem("Expand All");
0707: private JMenuItem expandAllBelow = new JMenuItem(
0708: "Expand All Below");
0709: private JMenuItem expandGoals = new JMenuItem(
0710: "Expand Goals Only");
0711: private JMenuItem expandGoalsBelow = new JMenuItem(
0712: "Expand Goals Only Below");
0713: private JMenuItem collapseAll = new JMenuItem("Collapse All");
0714: private JMenuItem collapseOtherBranches = new JMenuItem(
0715: "Collapse Other Branches");
0716: private JMenuItem collapseBelow = new JMenuItem(
0717: "Collapse Below");
0718: private JMenuItem prevSibling = new JMenuItem(
0719: "Previous Sibling");
0720: private JMenuItem nextSibling = new JMenuItem("Next Sibling");
0721: private JCheckBoxMenuItem hideIntermediate = new JCheckBoxMenuItem(
0722: "Hide Intermediate Proofsteps");
0723: private JCheckBoxMenuItem hideClosedSubtrees = new JCheckBoxMenuItem(
0724: "Hide Closed Subtrees");
0725: private JMenuItem search = new JMenuItem("Search");
0726: private JMenuItem goalBack = new JMenuItem("Prune Proof");
0727: private JMenuItem runStrategy = new JMenuItem("Apply Strategy",
0728: IconFactory.autoModeStartLogo(10));
0729: private JMenuItem mark = new JMenuItem("Mark for Re-Use");
0730: private JMenuItem visualize = new JMenuItem("Visualize");
0731: private JMenuItem test = new JMenuItem("Create Test For Node");
0732:
0733: private JMenuItem change = new JMenuItem("Change This Node");
0734:
0735: private TreePath path;
0736: private TreePath branch;
0737: private Node invokedNode;
0738:
0739: public ProofTreePopupMenu(TreePath p) {
0740: super ("Choose Action");
0741: path = p;
0742: delegateView.setSelectionPath(path);
0743: if (path.getLastPathComponent() instanceof GUIProofTreeNode) {
0744: branch = path.getParentPath();
0745: invokedNode = ((GUIProofTreeNode) path
0746: .getLastPathComponent()).getNode();
0747: } else {
0748: branch = path;
0749: invokedNode = ((GUIBranchNode) path
0750: .getLastPathComponent()).getNode();
0751: }
0752: create();
0753: search.setAccelerator(searchKeyStroke);
0754: }
0755:
0756: private void create() {
0757: this .add(expandAll);
0758: expandAll.addActionListener(this );
0759: this .add(expandAllBelow);
0760: expandAllBelow.addActionListener(this );
0761: this .add(expandGoals);
0762: expandGoals.addActionListener(this );
0763: this .add(expandGoalsBelow);
0764: expandGoalsBelow.addActionListener(this );
0765: this .add(collapseAll);
0766: collapseAll.addActionListener(this );
0767: this .add(collapseOtherBranches);
0768: collapseOtherBranches.addActionListener(this );
0769: this .add(collapseBelow);
0770: collapseBelow.addActionListener(this );
0771: this .add(new JSeparator());
0772: this .add(prevSibling);
0773: prevSibling.addActionListener(this );
0774: this .add(nextSibling);
0775: nextSibling.addActionListener(this );
0776: this .add(new JSeparator());
0777: this .add(hideIntermediate);
0778: hideIntermediate.setSelected(delegateModel
0779: .isHidingIntermediateProofsteps());
0780: hideIntermediate.addItemListener(this );
0781: this .add(hideClosedSubtrees);
0782: hideClosedSubtrees.setSelected(delegateModel
0783: .hideClosedSubtrees());
0784: hideClosedSubtrees.addItemListener(this );
0785: this .add(search);
0786: search.addActionListener(this );
0787: this .add(new JSeparator());
0788: this .add(goalBack);
0789: if (branch != path) {
0790: goalBack.addActionListener(this );
0791: goalBack.setEnabled(false);
0792: }
0793: this .add(runStrategy);
0794: runStrategy.addActionListener(this );
0795: runStrategy.setEnabled(false);
0796: if (proof != null) {
0797: //if (proof.getActiveStrategy() != null) {
0798: runStrategy.setEnabled(true);
0799: //}
0800: }
0801: if (branch != path) {
0802: this .add(visualize);
0803: visualize.addActionListener(this );
0804: visualize.setEnabled(true);
0805: ((ProofTreePopupMenu) this ).add(test);
0806: test.addActionListener(this );
0807: test.setEnabled(true);
0808: if (proof != null) {
0809: if (proof.isGoal(invokedNode)
0810: || proof.getSubtreeGoals(invokedNode)
0811: .size() > 0) {
0812: goalBack.setEnabled(true);
0813: }
0814: }
0815: this .add(change);
0816: change.addActionListener(this );
0817: this .add(mark);
0818: mark.addActionListener(this );
0819: }
0820: }
0821:
0822: public void actionPerformed(ActionEvent e) {
0823: if (e.getSource() == goalBack) {
0824: delegateModel.setAttentive(false);
0825: mediator().setBack(invokedNode);
0826: delegateModel.updateTree(null);
0827: delegateModel.setAttentive(true);
0828: makeNodeVisible(mediator.getSelectedNode());
0829: } else if (e.getSource() == runStrategy) {
0830: mediator().startAutoMode(
0831: proof.getSubtreeGoals(invokedNode));
0832: } else if (e.getSource() == mark) {
0833: mediator().mark(invokedNode);
0834: delegateView.treeDidChange(); // redraw with mark
0835: } else if (e.getSource() == expandAll) {
0836: ExpansionState.expandAll(delegateView);
0837: } else if (e.getSource() == expandAllBelow) {
0838: ExpansionState.expandAll(delegateView, branch);
0839: } else if (e.getSource() == expandGoals) {
0840: IteratorOfGoal it = proof.openGoals().iterator();
0841: Node n;
0842: while (it.hasNext()) {
0843: n = it.next().node();
0844: if (!mediator().getUserConstraint()
0845: .displayClosed(n))
0846: makeNodeExpanded(n);
0847: }
0848: collapseClosedNodes();
0849: // do not show selected node if it is not on the path to an
0850: // open goal, but do expand root
0851: // makeNodeVisible(mediator.getSelectedNode());
0852: delegateView.expandRow(0);
0853: } else if (e.getSource() == expandGoalsBelow) {
0854: Object tmpNode = branch.getLastPathComponent();
0855: if (branch == path) {
0856: ExpansionState.collapseAll(delegateView, branch);
0857: } else {
0858: for (int count = delegateModel
0859: .getChildCount(tmpNode), i = 0; i < count; i++) {
0860: Object child = delegateModel.getChild(tmpNode,
0861: i);
0862: if (!delegateModel.isLeaf(child))
0863: ExpansionState.collapseAll(delegateView,
0864: branch.pathByAddingChild(child));
0865: }
0866: }
0867: IteratorOfGoal it = proof.openGoals().iterator();
0868: Node n;
0869: while (it.hasNext()) {
0870: n = it.next().node();
0871: if (!mediator().getUserConstraint()
0872: .displayClosed(n)) {
0873: GUIProofTreeNode node = delegateModel
0874: .getProofTreeNode(n);
0875: if (node == null)
0876: break;
0877: Object[] obs = node.getPath();
0878: TreePath tp = new TreePath(obs);
0879: if (branch.isDescendant(tp)) {
0880: delegateView.makeVisible(tp);
0881: }
0882: }
0883: }
0884: } else if (e.getSource() == collapseAll) {
0885: ExpansionState.collapseAll(delegateView);
0886: delegateView.expandRow(0);
0887: } else if (e.getSource() == collapseOtherBranches) {
0888: collapseOthers(branch);
0889: } else if (e.getSource() == collapseBelow) {
0890: Object node = branch.getLastPathComponent();
0891:
0892: for (int count = delegateModel.getChildCount(node), i = 0; i < count; i++) {
0893: Object child = delegateModel.getChild(node, i);
0894:
0895: if (!delegateModel.isLeaf(child))
0896: ExpansionState.collapseAll(delegateView, branch
0897: .pathByAddingChild(child));
0898: }
0899: } else if (e.getSource() == prevSibling) {
0900: Object node = branch.getLastPathComponent();
0901: TreeNode parent = ((GUIAbstractTreeNode) node)
0902: .getParent();
0903: if (parent == null) {
0904: return;
0905: }
0906: Object sibling = delegateModel
0907: .getChild(parent, delegateModel
0908: .getIndexOfChild(parent, node) - 1);
0909: if (!(sibling != null && sibling instanceof GUIBranchNode)) {
0910: int index = delegateModel.getIndexOfChild(parent,
0911: node);
0912: for (int i = parent.getChildCount(); i > index; i--) {
0913: sibling = delegateModel.getChild(parent, i);
0914: if (sibling != null
0915: && sibling instanceof GUIBranchNode) {
0916: break;
0917: }
0918: }
0919: }
0920: if (sibling != null && sibling instanceof GUIBranchNode) {
0921: selectBranchNode((GUIBranchNode) sibling);
0922: }
0923: } else if (e.getSource() == nextSibling) {
0924: Object node = branch.getLastPathComponent();
0925: TreeNode parent = ((GUIAbstractTreeNode) node)
0926: .getParent();
0927: if (parent == null) {
0928: return;
0929: }
0930: Object sibling = delegateModel
0931: .getChild(parent, delegateModel
0932: .getIndexOfChild(parent, node) + 1);
0933: if (!(sibling != null && sibling instanceof GUIBranchNode)) {
0934: int index = delegateModel.getIndexOfChild(parent,
0935: node);
0936: for (int i = 0; i < index; i++) {
0937: sibling = delegateModel.getChild(parent, i);
0938: if (sibling != null
0939: && sibling instanceof GUIBranchNode) {
0940: break;
0941: }
0942: }
0943: }
0944: if (sibling != null && sibling instanceof GUIBranchNode) {
0945: selectBranchNode((GUIBranchNode) sibling);
0946: }
0947: } else if (e.getSource() == search) {
0948: proofTreeSearchPanel.setVisible(true);
0949: } else if (e.getSource() == visualize) {
0950: new ProofVisTreeView(mediator.visualizeProof()
0951: .getVisualizationModel());
0952: } else if (e.getSource() == test) {
0953: mediator.generateTestCaseForSelectedNode();
0954: } else if (e.getSource() == change) {
0955: mediator.changeNode(invokedNode);
0956: }
0957: }
0958:
0959: public void itemStateChanged(ItemEvent e) {
0960: if (e.getSource() == hideIntermediate) {
0961: delegateModel.hideIntermediateProofsteps(e
0962: .getStateChange() == ItemEvent.SELECTED);
0963: if (branch == path) {
0964: if (delegateModel.getRoot() instanceof GUIBranchNode) {
0965: TreeNode node = ((GUIAbstractTreeNode) delegateModel
0966: .getRoot()).findBranch(invokedNode);
0967: if (node instanceof GUIBranchNode) {
0968: selectBranchNode((GUIBranchNode) node);
0969: }
0970: }
0971: } else {
0972: delegateView.scrollPathToVisible(path);
0973: delegateView.setSelectionPath(path);
0974: }
0975: }
0976: if (e.getSource() == hideClosedSubtrees) {
0977: delegateModel
0978: .setHideClosedSubtrees(e.getStateChange() == ItemEvent.SELECTED);
0979: if (branch == path) {
0980: if (e.getStateChange() != ItemEvent.SELECTED) {
0981: if (delegateModel.getRoot() instanceof GUIBranchNode) {
0982: TreeNode node = ((GUIAbstractTreeNode) delegateModel
0983: .getRoot()).findBranch(invokedNode);
0984: if (node instanceof GUIBranchNode) {
0985: selectBranchNode((GUIBranchNode) node);
0986: }
0987: }
0988: } else {
0989: if (invokedNode.parent() == null
0990: || delegateModel
0991: .getProofTreeNode(
0992: invokedNode.parent())
0993: .findChild(invokedNode.parent()) == null) {
0994: // it's still a branch
0995: if (delegateModel.getRoot() instanceof GUIBranchNode) {
0996: TreeNode node = ((GUIAbstractTreeNode) delegateModel
0997: .getRoot())
0998: .findBranch(invokedNode);
0999: if (node instanceof GUIBranchNode) {
1000: selectBranchNode((GUIBranchNode) node);
1001: }
1002: }
1003: } else {
1004: TreePath tp = new TreePath(delegateModel
1005: .getProofTreeNode(invokedNode)
1006: .getPath());
1007: delegateView.scrollPathToVisible(tp);
1008: delegateView.setSelectionPath(tp);
1009: }
1010: }
1011: } else {
1012: TreePath tp = new TreePath(delegateModel
1013: .getProofTreeNode(invokedNode).getPath());
1014: delegateView.scrollPathToVisible(tp);
1015: delegateView.setSelectionPath(tp);
1016: }
1017: }
1018: }
1019:
1020: }
1021:
1022: class ProofTreeSearchPanel extends JPanel implements
1023: DocumentListener, TreeModelListener {
1024:
1025: private JTextField searchString = new JTextField(20);
1026: private JButton prev = new JButton("Prev");
1027: private JButton next = new JButton("Next");
1028: private JPanel panel = new JPanel();
1029: private JButton close = new JButton("Close");
1030: private int startRow = 0;
1031: private int currentRow = 0;
1032: private Position.Bias direction = Position.Bias.Forward;
1033: private ActionListener closePanel = new ActionListener() {
1034: public void actionPerformed(ActionEvent actionEvent) {
1035: setVisible(false);
1036: }
1037: };
1038: private ActionListener search = new ActionListener() {
1039: public void actionPerformed(ActionEvent e) {
1040: if (e.getSource() == next) {
1041: direction = Position.Bias.Forward;
1042: searchString.requestFocusInWindow();
1043: } else if (e.getSource() == prev) {
1044: direction = Position.Bias.Backward;
1045: searchString.requestFocusInWindow();
1046: } else {
1047: // if e.g. called by pressing enter, perform a forward search
1048: direction = Position.Bias.Forward;
1049: }
1050: searchNext();
1051: }
1052: };
1053:
1054: public ProofTreeSearchPanel() {
1055: registerKeyboardAction(closePanel, KeyStroke.getKeyStroke(
1056: KeyEvent.VK_ESCAPE, 0),
1057: JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT);
1058: registerKeyboardAction(search, KeyStroke.getKeyStroke(
1059: KeyEvent.VK_ENTER, 0),
1060: JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT);
1061: searchString.getDocument().addDocumentListener(this );
1062: prev.addActionListener(search);
1063: next.addActionListener(search);
1064: close.addActionListener(closePanel);
1065: setLayout(new BorderLayout());
1066: add(searchString, BorderLayout.NORTH);
1067: panel.setLayout(new BoxLayout(panel, BoxLayout.LINE_AXIS));
1068: panel.add(Box.createHorizontalGlue());
1069: panel.add(prev);
1070: panel.add(next);
1071: panel.add(Box.createHorizontalGlue());
1072: panel.add(close);
1073: add(panel, BorderLayout.SOUTH);
1074: super .setVisible(false);
1075: }
1076:
1077: public void setVisible(boolean vis) {
1078: super .setVisible(vis);
1079: if (vis) {
1080: searchString.selectAll();
1081: searchString.requestFocusInWindow();
1082: } else {
1083: delegateView.requestFocusInWindow();
1084: }
1085: }
1086:
1087: private synchronized void searchNext() {
1088: if (cache == null)
1089: fillCache();
1090: if (direction == Position.Bias.Forward) {
1091: if (currentRow + 1 < cache.size()) {
1092: startRow = currentRow + 1;
1093: } else {
1094: startRow = 0;
1095: }
1096: } else {
1097: if (currentRow - 1 >= 0) {
1098: startRow = currentRow - 1;
1099: } else {
1100: startRow = cache.size() - 1;
1101: }
1102: }
1103: search();
1104: }
1105:
1106: private synchronized void search() {
1107: if (searchString.getText().equals("")) {
1108: startRow = 0;
1109: }
1110: currentRow = getNextMatch(searchString.getText(), startRow,
1111: direction);
1112: GUIAbstractTreeNode node = null;
1113: TreePath tp = null;
1114: if (currentRow != -1) {
1115: node = (GUIAbstractTreeNode) cache.get(currentRow);
1116: tp = new TreePath(node.getPath());
1117: }
1118: if (node != null && node instanceof GUIBranchNode) {
1119: selectBranchNode((GUIBranchNode) node);
1120: } else {
1121: delegateView.scrollPathToVisible(tp);
1122: delegateView.setSelectionPath(tp);
1123: }
1124: }
1125:
1126: public void changedUpdate(DocumentEvent e) {
1127: search();
1128: }
1129:
1130: public void insertUpdate(DocumentEvent e) {
1131: search();
1132: }
1133:
1134: public void removeUpdate(DocumentEvent e) {
1135: search();
1136: }
1137:
1138: public void treeNodesChanged(TreeModelEvent e) {
1139: reset();
1140: }
1141:
1142: public void treeNodesInserted(TreeModelEvent e) {
1143: reset();
1144: }
1145:
1146: public void treeNodesRemoved(TreeModelEvent e) {
1147: reset();
1148: }
1149:
1150: public void treeStructureChanged(TreeModelEvent e) {
1151: reset();
1152: }
1153:
1154: private Vector cache;
1155:
1156: public synchronized void reset() {
1157: cache = null;
1158: }
1159:
1160: private void fillCache() {
1161: cache = new Vector();
1162: if (delegateModel.getRoot() != null) {
1163: cache
1164: .add((GUIAbstractTreeNode) delegateModel
1165: .getRoot());
1166: fillCacheHelp((GUIBranchNode) delegateModel.getRoot());
1167: }
1168: }
1169:
1170: private void fillCacheHelp(GUIBranchNode branch) {
1171: if (branch == null)
1172: return;
1173: GUIAbstractTreeNode n;
1174: for (int i = 0; i < delegateModel.getChildCount(branch); i++) {
1175: n = (GUIAbstractTreeNode) delegateModel.getChild(
1176: branch, i);
1177: cache.add(n);
1178: if (n instanceof GUIBranchNode)
1179: fillCacheHelp((GUIBranchNode) n);
1180: }
1181: }
1182:
1183: private int getNextMatch(String searchString, int startingRow,
1184: Position.Bias bias) {
1185: if (cache == null)
1186: fillCache();
1187: String s = searchString.toLowerCase();
1188:
1189: if (bias == Position.Bias.Forward) {
1190: if (startingRow < 0)
1191: startingRow = 0;
1192: for (int i = startingRow; i < cache.size(); i++) {
1193: if (containsString(cache.get(i).toString()
1194: .toLowerCase(), s))
1195: return i;
1196: }
1197: for (int i = 0; i < startingRow && i < cache.size(); i++) {
1198: if (containsString(cache.get(i).toString()
1199: .toLowerCase(), s))
1200: return i;
1201: }
1202: } else {
1203: if (startingRow > cache.size() - 1)
1204: startingRow = cache.size() - 1;
1205: for (int i = startingRow; i >= 0; i--) {
1206: if (containsString(cache.get(i).toString()
1207: .toLowerCase(), s))
1208: return i;
1209: }
1210: for (int i = cache.size() - 1; i > startingRow && i > 0; i--) {
1211: if (containsString(cache.get(i).toString()
1212: .toLowerCase(), s))
1213: return i;
1214: }
1215: }
1216: return -1;
1217: }
1218:
1219: /**
1220: * returns true if <tt>searchString</tt> is a substring of <tt>string</tt>
1221: * @param string the String where to search for an occurrence of <tt>searchString</tt>
1222: * @param searchString the String to be looked for
1223: * @return true if a match has been found
1224: */
1225: private boolean containsString(String string,
1226: String searchString) {
1227: assert string != null && searchString != null;
1228: return string.indexOf(searchString) != -1;
1229: }
1230:
1231: }
1232:
1233: }
|